CVC3  2.4.1
search.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file search.cpp
4  *
5  * Author: Clark Barrett, Vijay Ganesh (CNF Converter)
6  *
7  * Created: Fri Jan 17 14:19:54 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 
22 #include "search.h"
23 #include "search_rules.h"
24 #include "theory_core.h"
25 #include "eval_exception.h"
26 #include "theorem_manager.h"
27 #include "command_line_flags.h"
28 
29 
30 using namespace CVC3;
31 using namespace std;
32 
33 
34 //! Constructor
36  : d_core(core),
37  d_commonRules(core->getTM()->getRules())
38 {
39 
40  const CLFlags& flg = (core->getTM()->getFlags());
41  if (flg["lfsc-mode"].getInt()!= 0){
42  d_rules = createRules(this);
43 
44  }
45  else
46  d_rules = createRules();
47 
48 }
49 
50 
51 //! Destructor
53 {
54  delete d_rules;
55 }
56 
58 
59  if(!lastThm().isNull()) throw EvalException("Method tryModelGenereation() (or command COUNTERMODEL)\n must be called only after failed QUERY");
60 
61  // Save the scope level, to recover on errors
62  push();
64  bool success = d_core->refineCounterExample(thm);
65  if (!success) {
66  pop();
67  return false;
68  }
69 
70  QueryResult qres = checkValid(d_core->falseExpr(), thm);
71  if(qres == VALID) {
72  pop();
73  return false;
74  }
75 
76  success = d_core->buildModel(thm);
77  if (!success) {
78  pop();
79  return false;
80  }
81 
82  qres = checkValid(d_core->falseExpr(), thm);
83  if(qres == VALID) {
84  pop();
85  return false;
86  }
87 
88  return true;
89 }
90 
92 {
93  TRACE("model" , "Building a concrete model", "", "{");
94  if(!lastThm().isNull())
95  throw EvalException
96  ("Method getConcreteModel() (or command COUNTERMODEL)\n"
97  " must be called only after failed QUERY");
98  // Save the scope level, to recover on errors
99  push();
101  try {
103  } catch(Exception& e) {
104  // Clean up and re-throw the exception
105  pop();
106  throw e;
107  }
108  Theorem thm;
109  QueryResult qres = checkValid(d_core->falseExpr(), thm);
110  if(qres == VALID) {
111  vector<Expr> assump;
112  getAssumptions(assump);
114  Expr a = Expr(RAW_LIST, assump, d_core->getEM());
115  pop();
116  throw Exception
117  ("Model Creation failed after refining counterexample\n"
118  "due to the following assumptions:\n "
119  +a.toString()
120  +"\n\nYou might be using an incomplete fragment of the theory");
121  }
122 // else if (qres != INVALID) {
123 // throw EvalException
124 // ("Unable to build concrete model");
125 // }
126  try {
127  d_core->buildModel(m);
128  } catch(Exception& e) {
129  // Clean up and re-throw the exception
130  pop();
131  throw e;
132  }
133  qres = checkValid(d_core->falseExpr(), thm);
134  if(qres == VALID) {
135  vector<Expr> assump;
136  getAssumptions(assump);
137  Expr a = Expr(RAW_LIST, assump, d_core->getEM());
138  pop();
139  throw Exception
140  ("Model Creation failed due to the following assumptions:\n"
141  +a.toString()
142  +"\n\nYou might be using an incomplete fragment of the theory");
143  }
144 // else if (qres != INVALID) {
145 // throw EvalException
146 // ("Unable to build concrete model");
147 // }
148  TRACE("model" , "Building a concrete model", "", "}");
149 }
Data structure of expressions in CVC3.
Definition: expr.h:133
TheoremManager * getTM() const
Definition: theory_core.h:349
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
Abstract API to the proof search engine.
QueryResult
Definition: queryresult.h:32
void getConcreteModel(ExprMap< Expr > &m)
Build a concrete Model (assign values to variables), should only be called after a query which return...
Definition: search.cpp:91
void getLeafAssumptions(std::vector< Expr > &assumptions, bool negate=false) const
Definition: theorem.cpp:274
virtual void getAssumptions(std::vector< Expr > &assumptions)=0
Get all assumptions made in this and all previous contexts.
bool tryModelGeneration(Theorem &thm)
Try to build a concrete Model (assign values to variables), should only be called after a query which...
Definition: search.cpp:57
SearchEngineRules * d_rules
Proof rules for the search engine.
Definition: search.h:64
Abstract proof rules interface to the simple search engine.
virtual void pop()=0
Restore last checkpoint.
virtual void push()=0
Push a checkpoint.
virtual QueryResult checkValid(const Expr &e, Theorem &result)=0
Checks the validity of a formula in the current context.
virtual ~SearchEngine()
Destructor.
Definition: search.cpp:52
Definition: kinds.h:44
void refineCounterExample()
Calls for other theories to add facts to refine a coutnerexample.
SearchEngine(TheoryCore *core)
Constructor.
Definition: search.cpp:35
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
void collectBasicVars()
Split compound vars into basic type variables.
const Expr & falseExpr()
Return FALSE Expr.
Definition: theory.h:579
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
virtual Theorem lastThm()=0
Returns the result of the most recent valid theorem.
SearchEngineRules * createRules()
Create the trusted component.
Theorem inconsistentThm()
Get the proof of inconsistency for the current context.
Definition: theory_core.h:425
const CLFlags & getFlags() const
Definition: kinds.h:99
TheoryCore * d_core
Access to theory reasoning.
Definition: search.h:58
void buildModel(ExprMap< Expr > &m)
Calls theory specific computeModel, results are placed in map.