1 /********************* */
2 /*! \file smt_engine.cpp
4 ** Original author: mdeters
5 ** Major contributors: dejan
6 ** Minor contributors (to current version): cconway, kshitij
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief The main entry point into the CVC4 library's SMT interface
16 ** The main entry point into the CVC4 library's SMT interface.
25 #include <ext/hash_map>
27 #include "context/cdlist.h"
28 #include "context/cdhashset.h"
29 #include "context/context.h"
30 #include "decision/decision_engine.h"
31 #include "expr/command.h"
32 #include "expr/expr.h"
33 #include "expr/kind.h"
34 #include "expr/metakind.h"
35 #include "expr/node_builder.h"
36 #include "prop/prop_engine.h"
37 #include "smt/bad_option_exception.h"
38 #include "smt/modal_exception.h"
39 #include "smt/no_such_function_exception.h"
40 #include "smt/smt_engine.h"
41 #include "theory/theory_engine.h"
42 #include "proof/proof_manager.h"
43 #include "util/proof.h"
44 #include "util/boolean_simplification.h"
45 #include "util/configuration.h"
46 #include "util/exception.h"
47 #include "util/options.h"
48 #include "util/output.h"
49 #include "util/hash.h"
50 #include "theory/substitutions.h"
51 #include "theory/builtin/theory_builtin.h"
52 #include "theory/booleans/theory_bool.h"
53 #include "theory/booleans/circuit_propagator.h"
54 #include "theory/uf/theory_uf.h"
55 #include "theory/arith/theory_arith.h"
56 #include "theory/arrays/theory_arrays.h"
57 #include "theory/bv/theory_bv.h"
58 #include "theory/datatypes/theory_datatypes.h"
59 #include "theory/theory_traits.h"
60 #include "theory/logic_info.h"
61 #include "util/ite_removal.h"
65 using namespace CVC4::smt
;
66 using namespace CVC4::prop
;
67 using namespace CVC4::context
;
68 using namespace CVC4::theory
;
75 * Representation of a defined function. We keep these around in
76 * SmtEngine to permit expanding definitions late (and lazily), to
77 * support getValue() over defined functions, to support user output
78 * in terms of defined functions, etc.
80 class DefinedFunction
{
82 vector
<Node
> d_formals
;
86 DefinedFunction(Node func
, vector
<Node
> formals
, Node formula
) :
91 Node
getFunction() const { return d_func
; }
92 vector
<Node
> getFormals() const { return d_formals
; }
93 Node
getFormula() const { return d_formula
; }
94 };/* class DefinedFunction */
97 * This is an inelegant solution, but for the present, it will work.
98 * The point of this is to separate the public and private portions of
99 * the SmtEngine class, so that smt_engine.h doesn't
100 * include "expr/node.h", which is a private CVC4 header (and can lead
101 * to linking errors due to the improper inlining of non-visible symbols
104 * The "real" solution (that which is usually implemented) is to move
105 * ALL the implementation to SmtEnginePrivate and maintain a
106 * heap-allocated instance of it in SmtEngine. SmtEngine (the public
107 * one) becomes an "interface shell" which simply acts as a forwarder
110 class SmtEnginePrivate
{
113 /** The assertions yet to be preprocessed */
114 vector
<Node
> d_assertionsToPreprocess
;
116 /** Learned literals */
117 vector
<Node
> d_nonClausalLearnedLiterals
;
119 /** A circuit propagator for non-clausal propositional deduction */
120 booleans::CircuitPropagator d_propagator
;
122 /** Assertions to push to sat */
123 vector
<Node
> d_assertionsToCheck
;
125 /** Map from skolem variables to index in d_assertionsToCheck containing
126 * corresponding introduced Boolean ite */
127 IteSkolemMap d_iteSkolemMap
;
129 /** The top level substitutions */
130 theory::SubstitutionMap d_topLevelSubstitutions
;
133 * The last substitution that the SAT layer was told about.
134 * In incremental settings, substitutions cannot be performed
135 * "backward," only forward. So SAT needs to be told of all
136 * substitutions that are going to be done. This iterator
137 * holds the last substitution from d_topLevelSubstitutions
138 * that was pushed out to SAT.
139 * If d_lastSubstitutionPos == d_topLevelSubstitutions.end(),
140 * then nothing has been pushed out yet. */
141 context::CDO
<theory::SubstitutionMap::iterator
> d_lastSubstitutionPos
;
144 * Runs the nonclausal solver and tries to solve all the assigned
147 void nonClausalSimplify();
150 * Performs static learning on the assertions.
152 void staticLearning();
155 * Remove ITEs from the assertions.
159 // Simplify ITE structure
162 // Simplify based on unconstrained values
163 void unconstrainedSimp();
166 * Any variable in a assertion that is declared as a subtype type
167 * (predicate subtype or integer subrange type) must be constrained
168 * to be in that type.
170 void constrainSubtypes(TNode n
, std::vector
<Node
>& assertions
)
171 throw(AssertionException
);
174 * Perform non-clausal simplification of a Node. This involves
175 * Theory implementations, but does NOT involve the SAT solver in
178 void simplifyAssertions() throw(NoSuchFunctionException
, AssertionException
);
182 SmtEnginePrivate(SmtEngine
& smt
) :
184 d_nonClausalLearnedLiterals(),
185 d_propagator(smt
.d_userContext
, d_nonClausalLearnedLiterals
, true, true),
186 d_topLevelSubstitutions(smt
.d_userContext
),
187 d_lastSubstitutionPos(smt
.d_userContext
, d_topLevelSubstitutions
.end()) {
190 Node
applySubstitutions(TNode node
) const {
191 return Rewriter::rewrite(d_topLevelSubstitutions
.apply(node
));
195 * Process the assertions that have been asserted.
197 void processAssertions();
200 * Process a user pop. Clears out the non-context-dependent stuff in this
201 * SmtEnginePrivate. Necessary to clear out our assertion vectors in case
202 * someone does a push-assert-pop without a check-sat.
205 d_assertionsToPreprocess
.clear();
206 d_nonClausalLearnedLiterals
.clear();
207 d_assertionsToCheck
.clear();
211 * Adds a formula to the current context. Action here depends on
212 * the SimplificationMode (in the current Options scope); the
213 * formula might be pushed out to the propositional layer
214 * immediately, or it might be simplified and kept, or it might not
215 * even be simplified.
217 void addFormula(TNode n
)
218 throw(NoSuchFunctionException
, AssertionException
);
221 * Expand definitions in n.
223 Node
expandDefinitions(TNode n
, hash_map
<TNode
, Node
, TNodeHashFunction
>& cache
)
224 throw(NoSuchFunctionException
, AssertionException
);
226 };/* class SmtEnginePrivate */
228 }/* namespace CVC4::smt */
230 using namespace CVC4::smt
;
232 SmtEngine::SmtEngine(ExprManager
* em
) throw(AssertionException
) :
233 d_context(em
->getContext()),
235 d_userContext(new UserContext()),
237 d_nodeManager(d_exprManager
->getNodeManager()),
238 d_decisionEngine(NULL
),
239 d_theoryEngine(NULL
),
241 d_definedFunctions(NULL
),
242 d_assertionList(NULL
),
246 d_problemExtended(false),
248 d_needPostsolve(false),
249 d_timeBudgetCumulative(0),
250 d_timeBudgetPerCall(0),
251 d_resourceBudgetCumulative(0),
252 d_resourceBudgetPerCall(0),
253 d_cumulativeTimeUsed(0),
254 d_cumulativeResourceUsed(0),
256 d_private(new smt::SmtEnginePrivate(*this)),
257 d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
258 d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
259 d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
260 d_simpITETime("smt::SmtEngine::simpITETime"),
261 d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
262 d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
263 d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
264 d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
265 d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
266 d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
267 d_statResultSource("smt::resultSource", "unknown") {
269 NodeManagerScope
nms(d_nodeManager
);
271 StatisticsRegistry::registerStat(&d_definitionExpansionTime
);
272 StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime
);
273 StatisticsRegistry::registerStat(&d_staticLearningTime
);
274 StatisticsRegistry::registerStat(&d_simpITETime
);
275 StatisticsRegistry::registerStat(&d_unconstrainedSimpTime
);
276 StatisticsRegistry::registerStat(&d_iteRemovalTime
);
277 StatisticsRegistry::registerStat(&d_theoryPreprocessTime
);
278 StatisticsRegistry::registerStat(&d_cnfConversionTime
);
279 StatisticsRegistry::registerStat(&d_numAssertionsPre
);
280 StatisticsRegistry::registerStat(&d_numAssertionsPost
);
281 StatisticsRegistry::registerStat(&d_statResultSource
);
283 // We have mutual dependency here, so we add the prop engine to the theory
284 // engine later (it is non-essential there)
285 d_theoryEngine
= new TheoryEngine(d_context
, d_userContext
, const_cast<const LogicInfo
&>(d_logic
));
288 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
289 #undef CVC4_FOR_EACH_THEORY_STATEMENT
291 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
292 d_theoryEngine->addTheory<theory::TheoryTraits<THEORY>::theory_class>(THEORY);
293 CVC4_FOR_EACH_THEORY
;
295 d_decisionEngine
= new DecisionEngine(d_context
, d_userContext
);
296 d_propEngine
= new PropEngine(d_theoryEngine
, d_decisionEngine
, d_context
);
297 d_theoryEngine
->setPropEngine(d_propEngine
);
298 d_theoryEngine
->setDecisionEngine(d_decisionEngine
);
299 // d_decisionEngine->setPropEngine(d_propEngine);
301 // global push/pop around everything, to ensure proper destruction
302 // of context-dependent data structures
303 d_userContext
->push();
306 d_definedFunctions
= new(true) DefinedFunctionMap(d_userContext
);
308 // [MGD 10/20/2011] keep around in incremental mode, due to a
309 // cleanup ordering issue and Nodes/TNodes. If SAT is popped
310 // first, some user-context-dependent TNodes might still exist
312 if(Options::current()->interactive
||
313 Options::current()->incrementalSolving
) {
314 // In the case of incremental solving, we appear to need these to
315 // ensure the relevant Nodes remain live.
316 d_assertionList
= new(true) AssertionList(d_userContext
);
319 if(Options::current()->perCallResourceLimit
!= 0) {
320 setResourceLimit(Options::current()->perCallResourceLimit
, false);
322 if(Options::current()->cumulativeResourceLimit
!= 0) {
323 setResourceLimit(Options::current()->cumulativeResourceLimit
, true);
325 if(Options::current()->perCallMillisecondLimit
!= 0) {
326 setTimeLimit(Options::current()->perCallMillisecondLimit
, false);
328 if(Options::current()->cumulativeMillisecondLimit
!= 0) {
329 setTimeLimit(Options::current()->cumulativeMillisecondLimit
, true);
332 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(true));
333 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(false).notNode());
336 void SmtEngine::shutdown() {
337 if(Dump
.isOn("benchmark")) {
338 Dump("benchmark") << QuitCommand();
341 // check to see if a postsolve() is pending
342 if(d_needPostsolve
) {
343 d_theoryEngine
->postsolve();
344 d_needPostsolve
= false;
347 d_propEngine
->shutdown();
348 d_theoryEngine
->shutdown();
349 d_decisionEngine
->shutdown();
352 SmtEngine::~SmtEngine() throw() {
353 NodeManagerScope
nms(d_nodeManager
);
356 while(Options::current()->incrementalSolving
&& d_userContext
->getLevel() > 1) {
362 // global push/pop around everything, to ensure proper destruction
363 // of context-dependent data structures
365 d_userContext
->pop();
367 if(d_assignments
!= NULL
) {
368 d_assignments
->deleteSelf();
371 if(d_assertionList
!= NULL
) {
372 d_assertionList
->deleteSelf();
375 d_definedFunctions
->deleteSelf();
377 StatisticsRegistry::unregisterStat(&d_definitionExpansionTime
);
378 StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime
);
379 StatisticsRegistry::unregisterStat(&d_staticLearningTime
);
380 StatisticsRegistry::unregisterStat(&d_simpITETime
);
381 StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime
);
382 StatisticsRegistry::unregisterStat(&d_iteRemovalTime
);
383 StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime
);
384 StatisticsRegistry::unregisterStat(&d_cnfConversionTime
);
385 StatisticsRegistry::unregisterStat(&d_numAssertionsPre
);
386 StatisticsRegistry::unregisterStat(&d_numAssertionsPost
);
387 StatisticsRegistry::unregisterStat(&d_statResultSource
);
390 delete d_userContext
;
392 delete d_theoryEngine
;
394 //delete d_decisionEngine;
395 } catch(Exception
& e
) {
396 Warning() << "CVC4 threw an exception during cleanup." << endl
401 void SmtEngine::setLogic(const LogicInfo
& logic
) throw(ModalException
) {
402 NodeManagerScope
nms(d_nodeManager
);
405 throw ModalException("logic already set");
408 if(Dump
.isOn("benchmark")) {
409 Dump("benchmark") << SetBenchmarkLogicCommand(logic
.getLogicString());
412 setLogicInternal(logic
);
415 void SmtEngine::setLogic(const std::string
& s
) throw(ModalException
) {
416 NodeManagerScope
nms(d_nodeManager
);
418 setLogic(LogicInfo(s
));
421 void SmtEngine::setLogicInternal(const LogicInfo
& logic
) throw() {
424 // by default, symmetry breaker is on only for QF_UF
425 if(! Options::current()->ufSymmetryBreakerSetByUser
) {
426 bool qf_uf
= logic
.isPure(theory::THEORY_UF
) && !logic
.isQuantified();
427 Trace("smt") << "setting uf symmetry breaker to " << qf_uf
<< std::endl
;
428 NodeManager::currentNM()->getOptions()->ufSymmetryBreaker
= qf_uf
;
430 // by default, nonclausal simplification is off for QF_SAT
431 if(! Options::current()->simplificationModeSetByUser
) {
432 bool qf_sat
= logic
.isPure(theory::THEORY_BOOL
) && !logic
.isQuantified();
433 Trace("smt") << "setting simplification mode to <" << logic
.getLogicString() << "> " << (!qf_sat
) << std::endl
;
434 NodeManager::currentNM()->getOptions()->simplificationMode
= (qf_sat
? Options::SIMPLIFICATION_MODE_NONE
: Options::SIMPLIFICATION_MODE_BATCH
);
437 // If in arrays, set the UF handler to arrays
438 if(logic
.isPure(theory::THEORY_ARRAY
) && !logic
.isQuantified()) {
439 theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY
);
441 theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF
);
443 // Turn on ite simplification for QF_LIA and QF_AUFBV
444 if(! Options::current()->doITESimpSetByUser
) {
445 bool iteSimp
= !logic
.isQuantified() &&
446 ((logic
.isPure(theory::THEORY_ARITH
) && logic
.isLinear() && !logic
.isDifferenceLogic() && !logic
.areRealsUsed()) ||
447 (logic
.isTheoryEnabled(theory::THEORY_ARRAY
) && logic
.isTheoryEnabled(theory::THEORY_UF
) && logic
.isTheoryEnabled(theory::THEORY_BV
)));
448 Trace("smt") << "setting ite simplification to " << iteSimp
<< std::endl
;
449 NodeManager::currentNM()->getOptions()->doITESimp
= iteSimp
;
451 // Turn on multiple-pass non-clausal simplification for QF_AUFBV
452 if(! Options::current()->repeatSimpSetByUser
) {
453 bool repeatSimp
= !logic
.isQuantified() &&
454 (logic
.isTheoryEnabled(theory::THEORY_ARRAY
) && logic
.isTheoryEnabled(theory::THEORY_UF
) && logic
.isTheoryEnabled(theory::THEORY_BV
));
455 Trace("smt") << "setting repeat simplification to " << repeatSimp
<< std::endl
;
456 NodeManager::currentNM()->getOptions()->repeatSimp
= repeatSimp
;
458 // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode
459 if(! Options::current()->unconstrainedSimpSetByUser
|| Options::current()->incrementalSolving
) {
460 bool qf_sat
= logic
.isPure(theory::THEORY_BOOL
) && !logic
.isQuantified();
461 bool uncSimp
= false && !qf_sat
&& !Options::current()->incrementalSolving
;
462 Trace("smt") << "setting unconstrained simplification to " << uncSimp
<< std::endl
;
463 NodeManager::currentNM()->getOptions()->unconstrainedSimp
= uncSimp
;
465 // Turn on arith rewrite equalities only for pure arithmetic
466 if(! Options::current()->arithRewriteEqSetByUser
) {
467 bool arithRewriteEq
= logic
.isPure(theory::THEORY_ARITH
) && !logic
.isQuantified();
468 Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
<< std::endl
;
469 NodeManager::currentNM()->getOptions()->arithRewriteEq
= arithRewriteEq
;
474 void SmtEngine::setInfo(const std::string
& key
, const SExpr
& value
)
475 throw(BadOptionException
, ModalException
) {
476 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
477 if(Dump
.isOn("benchmark")) {
478 if(key
== ":status") {
479 std::string s
= value
.getValue();
480 BenchmarkStatus status
=
481 (s
== "sat") ? SMT_SATISFIABLE
:
482 ((s
== "unsat") ? SMT_UNSATISFIABLE
: SMT_UNKNOWN
);
483 Dump("benchmark") << SetBenchmarkStatusCommand(status
);
485 Dump("benchmark") << SetInfoCommand(key
, value
);
489 // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
490 if(key
.length() > 6) {
491 string prefix
= key
.substr(0, 6);
492 if(prefix
== ":cvc4-" || prefix
== ":cvc4_") {
493 string cvc4key
= key
.substr(6);
494 if(cvc4key
== "logic") {
495 if(! value
.isAtom()) {
496 throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string");
498 NodeManagerScope
nms(d_nodeManager
);
499 setLogicInternal(value
.getValue());
505 // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
508 key
== ":category" ||
509 key
== ":difficulty" ||
510 key
== ":smt-lib-version" ||
514 } else if(key
== ":status") {
517 s
= value
.getValue();
519 if(s
!= "sat" && s
!= "unsat" && s
!= "unknown") {
520 throw BadOptionException("argument to (set-info :status ..) must be "
521 "`sat' or `unsat' or `unknown'");
523 d_status
= Result(s
);
526 throw BadOptionException();
529 SExpr
SmtEngine::getInfo(const std::string
& key
) const
530 throw(BadOptionException
) {
531 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
532 if(key
== ":all-statistics") {
534 for(StatisticsRegistry::const_iterator i
= StatisticsRegistry::begin();
535 i
!= StatisticsRegistry::end();
538 v
.push_back((*i
)->getName());
539 v
.push_back((*i
)->getValue());
543 } else if(key
== ":error-behavior") {
544 return SExpr("immediate-exit");
545 } else if(key
== ":name") {
546 return Configuration::getName();
547 } else if(key
== ":version") {
548 return Configuration::getVersionString();
549 } else if(key
== ":authors") {
550 return Configuration::about();
551 } else if(key
== ":status") {
552 return d_status
.asSatisfiabilityResult().toString();
553 } else if(key
== ":reason-unknown") {
554 if(d_status
.isUnknown()) {
556 ss
<< d_status
.whyUnknown();
559 throw ModalException("Can't get-info :reason-unknown when the "
560 "last result wasn't unknown!");
563 throw BadOptionException();
567 void SmtEngine::setOption(const std::string
& key
, const SExpr
& value
)
568 throw(BadOptionException
, ModalException
) {
569 Trace("smt") << "SMT setOption(" << key
<< ", " << value
<< ")" << endl
;
570 if(Dump
.isOn("benchmark")) {
571 Dump("benchmark") << SetOptionCommand(key
, value
);
574 if(key
== ":print-success") {
575 if(value
.isAtom() && value
.getValue() == "false") {
576 // fine; don't need to do anything
578 throw BadOptionException();
580 } else if(key
== ":expand-definitions") {
581 throw BadOptionException();
582 } else if(key
== ":interactive-mode") {
583 throw BadOptionException();
584 } else if(key
== ":regular-output-channel") {
585 throw BadOptionException();
586 } else if(key
== ":diagnostic-output-channel") {
587 throw BadOptionException();
588 } else if(key
== ":random-seed") {
589 throw BadOptionException();
590 } else if(key
== ":verbosity") {
591 throw BadOptionException();
593 // The following options can only be set at the beginning; we throw
594 // a ModalException if someone tries.
596 throw ModalException("logic already set; cannot set options");
599 if(key
== ":produce-proofs") {
600 throw BadOptionException();
601 } else if(key
== ":produce-unsat-cores") {
602 throw BadOptionException();
603 } else if(key
== ":produce-models") {
604 throw BadOptionException();
605 } else if(key
== ":produce-assignments") {
606 throw BadOptionException();
608 throw BadOptionException();
613 SExpr
SmtEngine::getOption(const std::string
& key
) const
614 throw(BadOptionException
) {
615 Trace("smt") << "SMT getOption(" << key
<< ")" << endl
;
616 if(Dump
.isOn("benchmark")) {
617 Dump("benchmark") << GetOptionCommand(key
);
619 if(key
== ":print-success") {
620 return SExpr("true");
621 } else if(key
== ":expand-definitions") {
622 throw BadOptionException();
623 } else if(key
== ":interactive-mode") {
624 throw BadOptionException();
625 } else if(key
== ":produce-proofs") {
626 throw BadOptionException();
627 } else if(key
== ":produce-unsat-cores") {
628 throw BadOptionException();
629 } else if(key
== ":produce-models") {
630 throw BadOptionException();
631 } else if(key
== ":produce-assignments") {
632 throw BadOptionException();
633 } else if(key
== ":regular-output-channel") {
634 return SExpr("stdout");
635 } else if(key
== ":diagnostic-output-channel") {
636 return SExpr("stderr");
637 } else if(key
== ":random-seed") {
638 throw BadOptionException();
639 } else if(key
== ":verbosity") {
640 throw BadOptionException();
642 throw BadOptionException();
646 void SmtEngine::defineFunction(Expr func
,
647 const std::vector
<Expr
>& formals
,
649 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
650 if(Dump
.isOn("declarations")) {
652 ss
<< Expr::setlanguage(Expr::setlanguage::getLanguage(Dump
.getStream()))
654 Dump("declarations") << DefineFunctionCommand(ss
.str(), func
, formals
, formula
);
656 NodeManagerScope
nms(d_nodeManager
);
659 Type formulaType
= formula
.getType(Options::current()->typeChecking
);
661 Type funcType
= func
.getType();
662 Type rangeType
= funcType
.isFunction() ?
663 FunctionType(funcType
).getRangeType() : funcType
;
664 if(formulaType
!= rangeType
) {
666 ss
<< Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage
))
667 << "Defined function's declared type does not match that of body\n"
668 << "The function : " << func
<< "\n"
669 << "Its range type: " << rangeType
<< "\n"
670 << "The body : " << formula
<< "\n"
671 << "Body type : " << formulaType
;
672 throw TypeCheckingException(func
, ss
.str());
674 TNode funcNode
= func
.getTNode();
675 vector
<Node
> formalsNodes
;
676 for(vector
<Expr
>::const_iterator i
= formals
.begin(),
677 iend
= formals
.end();
680 formalsNodes
.push_back((*i
).getNode());
682 TNode formulaNode
= formula
.getTNode();
683 DefinedFunction
def(funcNode
, formalsNodes
, formulaNode
);
684 // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
685 // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
686 // d_haveAdditions = true;
687 d_definedFunctions
->insert(funcNode
, def
);
690 Node
SmtEnginePrivate::expandDefinitions(TNode n
, hash_map
<TNode
, Node
, TNodeHashFunction
>& cache
)
691 throw(NoSuchFunctionException
, AssertionException
) {
693 if(n
.getKind() != kind::APPLY
&& n
.getNumChildren() == 0) {
694 // don't bother putting in the cache
698 // maybe it's in the cache
699 hash_map
<TNode
, Node
, TNodeHashFunction
>::iterator cacheHit
= cache
.find(n
);
700 if(cacheHit
!= cache
.end()) {
701 TNode ret
= (*cacheHit
).second
;
702 return ret
.isNull() ? n
: ret
;
705 // otherwise expand it
706 if(n
.getKind() == kind::APPLY
) {
707 TNode func
= n
.getOperator();
708 SmtEngine::DefinedFunctionMap::const_iterator i
=
709 d_smt
.d_definedFunctions
->find(func
);
710 DefinedFunction def
= (*i
).second
;
711 vector
<Node
> formals
= def
.getFormals();
713 if(Debug
.isOn("expand")) {
714 Debug("expand") << "found: " << n
<< endl
;
715 Debug("expand") << " func: " << func
<< endl
;
716 string name
= func
.getAttribute(expr::VarNameAttr());
717 Debug("expand") << " : \"" << name
<< "\"" << endl
;
719 if(i
== d_smt
.d_definedFunctions
->end()) {
720 throw NoSuchFunctionException(Expr(d_smt
.d_exprManager
, new Node(func
)));
722 if(Debug
.isOn("expand")) {
723 Debug("expand") << " defn: " << def
.getFunction() << endl
725 if(formals
.size() > 0) {
726 copy( formals
.begin(), formals
.end() - 1,
727 ostream_iterator
<Node
>(Debug("expand"), ", ") );
728 Debug("expand") << formals
.back();
730 Debug("expand") << "]" << endl
731 << " " << def
.getFunction().getType() << endl
732 << " " << def
.getFormula() << endl
;
735 TNode fm
= def
.getFormula();
736 Node instance
= fm
.substitute(formals
.begin(), formals
.end(),
738 Debug("expand") << "made : " << instance
<< endl
;
740 Node expanded
= expandDefinitions(instance
, cache
);
741 cache
[n
] = (n
== expanded
? Node::null() : expanded
);
744 Debug("expand") << "cons : " << n
<< endl
;
745 NodeBuilder
<> nb(n
.getKind());
746 if(n
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
747 Debug("expand") << "op : " << n
.getOperator() << endl
;
748 nb
<< n
.getOperator();
750 for(TNode::iterator i
= n
.begin(),
754 Node expanded
= expandDefinitions(*i
, cache
);
755 Debug("expand") << "exchld: " << expanded
<< endl
;
759 cache
[n
] = n
== node
? Node::null() : node
;
765 void SmtEnginePrivate::removeITEs() {
766 Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl
;
768 // Remove all of the ITE occurrences and normalize
769 RemoveITE::run(d_assertionsToCheck
, d_iteSkolemMap
);
770 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
771 d_assertionsToCheck
[i
] = theory::Rewriter::rewrite(d_assertionsToCheck
[i
]);
776 void SmtEnginePrivate::staticLearning() {
778 TimerStat::CodeTimer
staticLearningTimer(d_smt
.d_staticLearningTime
);
780 Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl
;
782 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
784 NodeBuilder
<> learned(kind::AND
);
785 learned
<< d_assertionsToCheck
[i
];
786 d_smt
.d_theoryEngine
->ppStaticLearn(d_assertionsToCheck
[i
], learned
);
787 if(learned
.getNumChildren() == 1) {
790 d_assertionsToCheck
[i
] = learned
;
795 void SmtEnginePrivate::nonClausalSimplify() {
797 TimerStat::CodeTimer
nonclausalTimer(d_smt
.d_nonclausalSimplificationTime
);
799 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl
;
801 // Apply the substitutions we already have, and normalize
802 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
803 << "applying substitutions" << endl
;
804 for (unsigned i
= 0; i
< d_assertionsToPreprocess
.size(); ++ i
) {
805 Trace("simplify") << "applying to " << d_assertionsToPreprocess
[i
] << endl
;
806 d_assertionsToPreprocess
[i
] =
807 theory::Rewriter::rewrite(d_topLevelSubstitutions
.apply(d_assertionsToPreprocess
[i
]));
808 Trace("simplify") << " got " << d_assertionsToPreprocess
[i
] << endl
;
811 // Assert all the assertions to the propagator
812 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
813 << "asserting to propagator" << endl
;
814 for (unsigned i
= 0; i
< d_assertionsToPreprocess
.size(); ++ i
) {
815 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess
[i
] << endl
;
816 d_propagator
.assert(d_assertionsToPreprocess
[i
]);
819 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
820 << "propagating" << endl
;
821 if (d_propagator
.propagate()) {
822 // If in conflict, just return false
823 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
824 << "conflict in non-clausal propagation" << endl
;
825 d_assertionsToPreprocess
.clear();
826 d_assertionsToCheck
.push_back(NodeManager::currentNM()->mkConst
<bool>(false));
829 // No, conflict, go through the literals and solve them
831 for(unsigned i
= 0, i_end
= d_nonClausalLearnedLiterals
.size(); i
< i_end
; ++ i
) {
832 // Simplify the literal we learned wrt previous substitutions
833 Node learnedLiteral
=
834 theory::Rewriter::rewrite(d_topLevelSubstitutions
.apply(d_nonClausalLearnedLiterals
[i
]));
835 // It might just simplify to a constant
836 if (learnedLiteral
.isConst()) {
837 if (learnedLiteral
.getConst
<bool>()) {
838 // If the learned literal simplifies to true, it's redundant
841 // If the learned literal simplifies to false, we're in conflict
842 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
844 << d_nonClausalLearnedLiterals
[i
] << endl
;
845 d_assertionsToPreprocess
.clear();
846 d_assertionsToCheck
.push_back(NodeManager::currentNM()->mkConst
<bool>(false));
850 // Solve it with the corresponding theory
851 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
852 << "solving " << learnedLiteral
<< endl
;
853 Theory::PPAssertStatus solveStatus
=
854 d_smt
.d_theoryEngine
->solve(learnedLiteral
, d_topLevelSubstitutions
);
856 switch (solveStatus
) {
857 case Theory::PP_ASSERT_STATUS_CONFLICT
:
858 // If in conflict, we return false
859 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
860 << "conflict while solving "
861 << learnedLiteral
<< endl
;
862 d_assertionsToPreprocess
.clear();
863 d_assertionsToCheck
.push_back(NodeManager::currentNM()->mkConst
<bool>(false));
865 case Theory::PP_ASSERT_STATUS_SOLVED
:
866 // The literal should rewrite to true
867 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
868 << "solved " << learnedLiteral
<< endl
;
869 Assert(theory::Rewriter::rewrite(d_topLevelSubstitutions
.apply(learnedLiteral
)).isConst());
873 d_nonClausalLearnedLiterals
[j
++] = d_nonClausalLearnedLiterals
[i
];
877 if( Options::current()->incrementalSolving
||
878 Options::current()->simplificationMode
== Options::SIMPLIFICATION_MODE_INCREMENTAL
) {
879 // Tell PropEngine about new substitutions
880 SubstitutionMap::iterator pos
= d_lastSubstitutionPos
;
881 if(pos
== d_topLevelSubstitutions
.end()) {
882 pos
= d_topLevelSubstitutions
.begin();
887 while(pos
!= d_topLevelSubstitutions
.end()) {
888 // Push out this substitution
889 TNode lhs
= (*pos
).first
, rhs
= (*pos
).second
;
890 Node n
= NodeManager::currentNM()->mkNode(lhs
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, lhs
, rhs
);
891 d_assertionsToCheck
.push_back(n
);
892 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n
<< endl
;
893 d_lastSubstitutionPos
= pos
;
899 d_nonClausalLearnedLiterals
.resize(j
);
902 hash_set
<TNode
, TNodeHashFunction
> s
;
903 for (unsigned i
= 0; i
< d_assertionsToPreprocess
.size(); ++ i
) {
904 Node assertion
= theory::Rewriter::rewrite(d_topLevelSubstitutions
.apply(d_assertionsToPreprocess
[i
]));
906 d_assertionsToCheck
.push_back(assertion
);
907 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
908 << "non-clausal preprocessed: "
909 << assertion
<< endl
;
911 d_assertionsToPreprocess
.clear();
913 for (unsigned i
= 0; i
< d_nonClausalLearnedLiterals
.size(); ++ i
) {
914 Node learned
= theory::Rewriter::rewrite(d_topLevelSubstitutions
.apply(d_nonClausalLearnedLiterals
[i
]));
915 if (s
.find(learned
) != s
.end()) {
919 d_assertionsToCheck
.push_back(learned
);
920 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
921 << "non-clausal learned : "
922 << d_assertionsToCheck
.back() << endl
;
924 d_nonClausalLearnedLiterals
.clear();
928 void SmtEnginePrivate::simpITE()
930 TimerStat::CodeTimer
simpITETimer(d_smt
.d_simpITETime
);
932 Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl
;
934 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
936 d_assertionsToCheck
[i
] = d_smt
.d_theoryEngine
->ppSimpITE(d_assertionsToCheck
[i
]);
941 void SmtEnginePrivate::unconstrainedSimp()
943 TimerStat::CodeTimer
unconstrainedSimpTimer(d_smt
.d_unconstrainedSimpTime
);
945 Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl
;
946 d_smt
.d_theoryEngine
->ppUnconstrainedSimp(d_assertionsToCheck
);
950 void SmtEnginePrivate::constrainSubtypes(TNode top
, std::vector
<Node
>& assertions
)
951 throw(AssertionException
) {
953 Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top
<< endl
;
956 stack
<TNode
> worklist
;
961 TNode n
= worklist
.top();
964 TypeNode t
= n
.getType();
965 if(t
.isPredicateSubtype()) {
966 WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl
;
967 Node pred
= t
.getSubtypePredicate();
969 // pred can be a LAMBDA, a function constant, or a datatype tester
970 Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred
.getType() << endl
;
971 if(d_smt
.d_definedFunctions
->find(pred
) != d_smt
.d_definedFunctions
->end()) {
973 } else if(pred
.getType().isTester()) {
974 k
= kind::APPLY_TESTER
;
978 Node app
= NodeManager::currentNM()->mkNode(k
, pred
, n
);
979 Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k
<< ") " << app
<< endl
;
980 assertions
.push_back(app
);
981 } else if(t
.isSubrange()) {
982 SubrangeBounds bounds
= t
.getSubrangeBounds();
983 Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds
<< endl
;
984 if(bounds
.lower
.hasBound()) {
985 Node c
= NodeManager::currentNM()->mkConst(Rational(bounds
.lower
.getBound()));
986 Node lb
= NodeManager::currentNM()->mkNode(kind::LEQ
, c
, n
);
987 Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb
<< endl
;
988 assertions
.push_back(lb
);
990 if(bounds
.upper
.hasBound()) {
991 Node c
= NodeManager::currentNM()->mkConst(Rational(bounds
.upper
.getBound()));
992 Node ub
= NodeManager::currentNM()->mkNode(kind::LEQ
, n
, c
);
993 Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub
<< endl
;
994 assertions
.push_back(ub
);
998 for(TNode::iterator i
= n
.begin(); i
!= n
.end(); ++i
) {
999 if(done
.find(*i
) == done
.end()) {
1004 } while(! worklist
.empty());
1007 void SmtEnginePrivate::simplifyAssertions()
1008 throw(NoSuchFunctionException
, AssertionException
) {
1011 Trace("simplify") << "SmtEnginePrivate::simplify()" << endl
;
1013 if(!Options::current()->lazyDefinitionExpansion
) {
1014 Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl
;
1015 TimerStat::CodeTimer
codeTimer(d_smt
.d_definitionExpansionTime
);
1016 hash_map
<TNode
, Node
, TNodeHashFunction
> cache
;
1017 for (unsigned i
= 0; i
< d_assertionsToPreprocess
.size(); ++ i
) {
1018 d_assertionsToPreprocess
[i
] =
1019 expandDefinitions(d_assertionsToPreprocess
[i
], cache
);
1023 if(Options::current()->simplificationMode
!= Options::SIMPLIFICATION_MODE_NONE
) {
1024 // Perform non-clausal simplification
1025 Trace("simplify") << "SmtEnginePrivate::simplify(): "
1026 << "performing non-clausal simplification" << endl
;
1027 // Abuse the user context to make sure circuit propagator gets backtracked
1028 d_smt
.d_userContext
->push();
1029 nonClausalSimplify();
1030 d_smt
.d_userContext
->pop();
1032 Assert(d_assertionsToCheck
.empty());
1033 d_assertionsToCheck
.swap(d_assertionsToPreprocess
);
1036 if(Options::current()->doITESimp
) {
1037 // ite simplification
1041 if(Options::current()->unconstrainedSimp
) {
1042 unconstrainedSimp();
1045 if(Options::current()->repeatSimp
&& Options::current()->simplificationMode
!= Options::SIMPLIFICATION_MODE_NONE
) {
1046 d_assertionsToCheck
.swap(d_assertionsToPreprocess
);
1047 // Abuse the user context to make sure circuit propagator gets backtracked
1048 d_smt
.d_userContext
->push();
1049 nonClausalSimplify();
1050 d_smt
.d_userContext
->pop();
1053 if(Options::current()->doStaticLearning
) {
1054 // Perform static learning
1055 Trace("simplify") << "SmtEnginePrivate::simplify(): "
1056 << "performing static learning" << endl
;
1060 } catch(TypeCheckingExceptionPrivate
& tcep
) {
1061 // Calls to this function should have already weeded out any
1062 // typechecking exceptions via (e.g.) ensureBoolean(). But a
1063 // theory could still create a new expression that isn't
1064 // well-typed, and we don't want the C++ runtime to abort our
1065 // process without any error notice.
1067 ss
<< Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage
))
1068 << "A bad expression was produced. Original exception follows:\n"
1070 InternalError(ss
.str().c_str());
1074 Result
SmtEngine::check() {
1075 Trace("smt") << "SmtEngine::check()" << endl
;
1077 // Make sure the prop layer has all of the assertions
1078 Trace("smt") << "SmtEngine::check(): processing assertions" << endl
;
1079 d_private
->processAssertions();
1081 unsigned long millis
= 0;
1082 if(d_timeBudgetCumulative
!= 0) {
1083 millis
= getTimeRemaining();
1085 return Result(Result::VALIDITY_UNKNOWN
, Result::TIMEOUT
);
1088 if(d_timeBudgetPerCall
!= 0 && (millis
== 0 || d_timeBudgetPerCall
< millis
)) {
1089 millis
= d_timeBudgetPerCall
;
1092 unsigned long resource
= 0;
1093 if(d_resourceBudgetCumulative
!= 0) {
1094 resource
= getResourceRemaining();
1096 return Result(Result::VALIDITY_UNKNOWN
, Result::RESOURCEOUT
);
1099 if(d_resourceBudgetPerCall
!= 0 && (resource
== 0 || d_resourceBudgetPerCall
< resource
)) {
1100 resource
= d_resourceBudgetPerCall
;
1103 Trace("smt") << "SmtEngine::check(): running check" << endl
;
1104 Result result
= d_propEngine
->checkSat(millis
, resource
);
1105 d_statResultSource
.setData("satSolver");
1107 // PropEngine::checkSat() returns the actual amount used in these
1109 d_cumulativeTimeUsed
+= millis
;
1110 d_cumulativeResourceUsed
+= resource
;
1112 Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
1113 << ", conflicts " << d_cumulativeResourceUsed
<< endl
;
1115 if(result
.isUnknown() and d_decisionEngine
!= NULL
) {
1116 Result deResult
= d_decisionEngine
->getResult();
1117 if(not deResult
.isUnknown()) {
1118 d_statResultSource
.setData("decisionEngine");
1126 Result
SmtEngine::quickCheck() {
1127 Trace("smt") << "SMT quickCheck()" << endl
;
1128 return Result(Result::VALIDITY_UNKNOWN
, Result::REQUIRES_FULL_CHECK
);
1131 void SmtEnginePrivate::processAssertions() {
1133 Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl
;
1135 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
1136 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
1138 // Any variables of subtype types need to be constrained properly.
1139 // Careful, here: constrainSubtypes() adds to the back of
1140 // d_assertionsToPreprocess, but we don't need to reprocess those.
1141 // We also can't use an iterator, because the vector may be moved in
1142 // memory during this loop.
1143 for(unsigned i
= 0, i_end
= d_assertionsToPreprocess
.size(); i
!= i_end
; ++i
) {
1144 constrainSubtypes(d_assertionsToPreprocess
[i
], d_assertionsToPreprocess
);
1147 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
1148 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
1150 // Simplify the assertions
1151 simplifyAssertions();
1153 // any assertions beyond realAssertionsEnd _must_ be introduced by
1155 int realAssertionsEnd
= d_assertionsToCheck
.size();
1158 TimerStat::CodeTimer
codeTimer(d_smt
.d_iteRemovalTime
);
1160 d_smt
.d_numAssertionsPre
+= d_assertionsToCheck
.size();
1161 // Remove ITEs, updating d_iteSkolemMap
1163 d_smt
.d_numAssertionsPost
+= d_assertionsToCheck
.size();
1164 // This may need to be in a try-catch
1165 // block. make regress is passing, so
1166 // skipping for now --K
1169 if(Options::current()->repeatSimp
) {
1170 d_assertionsToCheck
.swap(d_assertionsToPreprocess
);
1171 simplifyAssertions();
1175 // begin: INVARIANT to maintain: no reordering of assertions or
1176 // introducing new ones
1177 #ifdef CVC4_ASSERTIONS
1178 unsigned iteRewriteAssertionsEnd
= d_assertionsToCheck
.size();
1181 Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl
;
1182 Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess
.size() << endl
;
1183 Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck
.size() << endl
;
1185 if(Dump
.isOn("assertions")) {
1186 // Push the simplified assertions to the dump output stream
1187 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
1189 << AssertCommand(BoolExpr(d_assertionsToCheck
[i
].toExpr()));
1194 TimerStat::CodeTimer
codeTimer(d_smt
.d_theoryPreprocessTime
);
1195 // Call the theory preprocessors
1196 d_smt
.d_theoryEngine
->preprocessStart();
1197 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
1198 d_assertionsToCheck
[i
] = d_smt
.d_theoryEngine
->preprocess(d_assertionsToCheck
[i
]);
1202 // Push the formula to decision engine
1203 Assert(iteRewriteAssertionsEnd
== d_assertionsToCheck
.size());
1204 d_smt
.d_decisionEngine
->addAssertions
1205 (d_assertionsToCheck
, realAssertionsEnd
, d_iteSkolemMap
);
1207 // end: INVARIANT to maintain: no reordering of assertions or
1208 // introducing new ones
1210 // Push the formula to SAT
1212 TimerStat::CodeTimer
codeTimer(d_smt
.d_cnfConversionTime
);
1213 for (unsigned i
= 0; i
< d_assertionsToCheck
.size(); ++ i
) {
1214 d_smt
.d_propEngine
->assertFormula(d_assertionsToCheck
[i
]);
1218 d_assertionsToCheck
.clear();
1219 d_iteSkolemMap
.clear();
1222 void SmtEnginePrivate::addFormula(TNode n
)
1223 throw(NoSuchFunctionException
, AssertionException
) {
1225 Trace("smt") << "SmtEnginePrivate::addFormula(" << n
<< ")" << endl
;
1227 // Add the normalized formula to the queue
1228 d_assertionsToPreprocess
.push_back(theory::Rewriter::rewrite(n
));
1230 // If the mode of processing is incremental prepreocess and assert immediately
1231 if (Options::current()->simplificationMode
== Options::SIMPLIFICATION_MODE_INCREMENTAL
) {
1232 processAssertions();
1236 void SmtEngine::ensureBoolean(const BoolExpr
& e
) {
1237 Type type
= e
.getType(Options::current()->typeChecking
);
1238 Type boolType
= d_exprManager
->booleanType();
1239 if(type
!= boolType
) {
1241 ss
<< Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage
))
1242 << "Expected " << boolType
<< "\n"
1243 << "The assertion : " << e
<< "\n"
1244 << "Its type : " << type
;
1245 throw TypeCheckingException(e
, ss
.str());
1249 Result
SmtEngine::checkSat(const BoolExpr
& e
) {
1251 Assert(e
.isNull() || e
.getExprManager() == d_exprManager
);
1253 NodeManagerScope
nms(d_nodeManager
);
1255 Trace("smt") << "SmtEngine::checkSat(" << e
<< ")" << endl
;
1257 if(d_queryMade
&& !Options::current()->incrementalSolving
) {
1258 throw ModalException("Cannot make multiple queries unless "
1259 "incremental solving is enabled "
1260 "(try --incremental)");
1263 // Ensure that the expression is type-checked at this point, and Boolean
1268 // check to see if a postsolve() is pending
1269 if(d_needPostsolve
) {
1270 d_theoryEngine
->postsolve();
1271 d_needPostsolve
= false;
1277 // Note that a query has been made
1282 d_problemExtended
= true;
1283 d_private
->addFormula(e
.getNode());
1287 Result r
= check().asSatisfiabilityResult();
1288 d_needPostsolve
= true;
1290 // Dump the query if requested
1291 if(Dump
.isOn("benchmark")) {
1292 // the expr already got dumped out if assertion-dumping is on
1293 Dump("benchmark") << CheckSatCommand();
1299 // Remember the status
1302 d_problemExtended
= false;
1304 Trace("smt") << "SmtEngine::checkSat(" << e
<< ") => " << r
<< endl
;
1309 Result
SmtEngine::query(const BoolExpr
& e
) {
1311 Assert(!e
.isNull());
1312 Assert(e
.getExprManager() == d_exprManager
);
1314 NodeManagerScope
nms(d_nodeManager
);
1316 Trace("smt") << "SMT query(" << e
<< ")" << endl
;
1318 if(d_queryMade
&& !Options::current()->incrementalSolving
) {
1319 throw ModalException("Cannot make multiple queries unless "
1320 "incremental solving is enabled "
1321 "(try --incremental)");
1324 // Ensure that the expression is type-checked at this point, and Boolean
1327 // check to see if a postsolve() is pending
1328 if(d_needPostsolve
) {
1329 d_theoryEngine
->postsolve();
1330 d_needPostsolve
= false;
1336 // Note that a query has been made
1340 d_problemExtended
= true;
1341 d_private
->addFormula(e
.getNode().notNode());
1344 Result r
= check().asValidityResult();
1345 d_needPostsolve
= true;
1347 // Dump the query if requested
1348 if(Dump
.isOn("benchmark")) {
1349 // the expr already got dumped out if assertion-dumping is on
1350 Dump("benchmark") << CheckSatCommand();
1356 // Remember the status
1359 d_problemExtended
= false;
1361 Trace("smt") << "SMT query(" << e
<< ") ==> " << r
<< endl
;
1366 Result
SmtEngine::assertFormula(const BoolExpr
& e
) {
1367 Assert(e
.getExprManager() == d_exprManager
);
1368 NodeManagerScope
nms(d_nodeManager
);
1369 Trace("smt") << "SmtEngine::assertFormula(" << e
<< ")" << endl
;
1371 if(d_assertionList
!= NULL
) {
1372 d_assertionList
->push_back(e
);
1374 d_private
->addFormula(e
.getNode());
1375 return quickCheck().asValidityResult();
1378 Expr
SmtEngine::simplify(const Expr
& e
) {
1379 Assert(e
.getExprManager() == d_exprManager
);
1380 NodeManagerScope
nms(d_nodeManager
);
1381 if( Options::current()->typeChecking
) {
1382 e
.getType(true);// ensure expr is type-checked at this point
1384 Trace("smt") << "SMT simplify(" << e
<< ")" << endl
;
1385 if(Dump
.isOn("benchmark")) {
1386 Dump("benchmark") << SimplifyCommand(e
);
1388 return d_private
->applySubstitutions(e
).toExpr();
1391 Expr
SmtEngine::getValue(const Expr
& e
)
1392 throw(ModalException
, AssertionException
) {
1393 Assert(e
.getExprManager() == d_exprManager
);
1394 NodeManagerScope
nms(d_nodeManager
);
1396 // ensure expr is type-checked at this point
1397 Type type
= e
.getType(Options::current()->typeChecking
);
1399 Trace("smt") << "SMT getValue(" << e
<< ")" << endl
;
1400 if(Dump
.isOn("benchmark")) {
1401 Dump("benchmark") << GetValueCommand(e
);
1403 if(!Options::current()->produceModels
) {
1405 "Cannot get value when produce-models options is off.";
1406 throw ModalException(msg
);
1408 if(d_status
.isNull() ||
1409 d_status
.asSatisfiabilityResult() != Result::SAT
||
1410 d_problemExtended
) {
1412 "Cannot get value unless immediately preceded by SAT/INVALID response.";
1413 throw ModalException(msg
);
1415 if(type
.isFunction() || type
.isPredicate() ||
1416 type
.isKind() || type
.isSortConstructor()) {
1418 "Cannot get value of a function, predicate, or sort.";
1419 throw ModalException(msg
);
1422 // Apply what was learned from preprocessing
1423 Node n
= d_private
->applySubstitutions(e
.getNode());
1425 // Normalize for the theories
1426 n
= theory::Rewriter::rewrite(n
);
1428 Trace("smt") << "--- getting value of " << n
<< endl
;
1429 Node resultNode
= d_theoryEngine
->getValue(n
);
1431 // type-check the result we got
1432 Assert(resultNode
.isNull() || resultNode
.getType() == n
.getType());
1433 return Expr(d_exprManager
, new Node(resultNode
));
1436 bool SmtEngine::addToAssignment(const Expr
& e
) throw(AssertionException
) {
1437 NodeManagerScope
nms(d_nodeManager
);
1438 Type type
= e
.getType(Options::current()->typeChecking
);
1440 CheckArgument( type
.isBoolean(), e
,
1441 "expected Boolean-typed variable or function application "
1442 "in addToAssignment()" );
1443 Node n
= e
.getNode();
1444 // must be an APPLY of a zero-ary defined function, or a variable
1445 CheckArgument( ( ( n
.getKind() == kind::APPLY
&&
1446 ( d_definedFunctions
->find(n
.getOperator()) !=
1447 d_definedFunctions
->end() ) &&
1448 n
.getNumChildren() == 0 ) ||
1449 n
.getMetaKind() == kind::metakind::VARIABLE
), e
,
1450 "expected variable or defined-function application "
1451 "in addToAssignment(),\ngot %s", e
.toString().c_str() );
1452 if(!Options::current()->produceAssignments
) {
1455 if(d_assignments
== NULL
) {
1456 d_assignments
= new(true) AssignmentSet(d_context
);
1458 d_assignments
->insert(n
);
1463 SExpr
SmtEngine::getAssignment() throw(ModalException
, AssertionException
) {
1464 Trace("smt") << "SMT getAssignment()" << endl
;
1465 NodeManagerScope
nms(d_nodeManager
);
1466 if(Dump
.isOn("benchmark")) {
1467 Dump("benchmark") << GetAssignmentCommand();
1469 if(!Options::current()->produceAssignments
) {
1471 "Cannot get the current assignment when "
1472 "produce-assignments option is off.";
1473 throw ModalException(msg
);
1475 if(d_status
.isNull() ||
1476 d_status
.asSatisfiabilityResult() != Result::SAT
||
1477 d_problemExtended
) {
1479 "Cannot get the current assignment unless immediately "
1480 "preceded by SAT/INVALID response.";
1481 throw ModalException(msg
);
1484 if(d_assignments
== NULL
) {
1488 vector
<SExpr
> sexprs
;
1489 TypeNode boolType
= d_nodeManager
->booleanType();
1490 for(AssignmentSet::const_iterator i
= d_assignments
->begin(),
1491 iend
= d_assignments
->end();
1494 Assert((*i
).getType() == boolType
);
1497 Node n
= theory::Rewriter::rewrite(*i
);
1499 Trace("smt") << "--- getting value of " << n
<< endl
;
1500 Node resultNode
= d_theoryEngine
->getValue(n
);
1502 // type-check the result we got
1503 Assert(resultNode
.isNull() || resultNode
.getType() == boolType
);
1506 if((*i
).getKind() == kind::APPLY
) {
1507 Assert((*i
).getNumChildren() == 0);
1508 v
.push_back((*i
).getOperator().toString());
1510 Assert((*i
).getMetaKind() == kind::metakind::VARIABLE
);
1511 v
.push_back((*i
).toString());
1513 v
.push_back(resultNode
.toString());
1514 sexprs
.push_back(v
);
1516 return SExpr(sexprs
);
1519 Proof
* SmtEngine::getProof() throw(ModalException
, AssertionException
) {
1520 Trace("smt") << "SMT getProof()" << endl
;
1521 NodeManagerScope
nms(d_nodeManager
);
1522 if(Dump
.isOn("benchmark")) {
1523 Dump("benchmark") << GetProofCommand();
1526 if(!Options::current()->proof
) {
1528 "Cannot get a proof when produce-proofs option is off.";
1529 throw ModalException(msg
);
1531 if(d_status
.isNull() ||
1532 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
1533 d_problemExtended
) {
1535 "Cannot get a proof unless immediately preceded by UNSAT/VALID response.";
1536 throw ModalException(msg
);
1539 return ProofManager::getProof();
1540 #else /* CVC4_PROOF */
1541 throw ModalException("This build of CVC4 doesn't have proof support.");
1542 #endif /* CVC4_PROOF */
1545 vector
<Expr
> SmtEngine::getAssertions()
1546 throw(ModalException
, AssertionException
) {
1547 if(Dump
.isOn("benchmark")) {
1548 Dump("benchmark") << GetAssertionsCommand();
1550 NodeManagerScope
nms(d_nodeManager
);
1551 Trace("smt") << "SMT getAssertions()" << endl
;
1552 if(!Options::current()->interactive
) {
1554 "Cannot query the current assertion list when not in interactive mode.";
1555 throw ModalException(msg
);
1557 Assert(d_assertionList
!= NULL
);
1558 return vector
<Expr
>(d_assertionList
->begin(), d_assertionList
->end());
1561 size_t SmtEngine::getStackLevel() const {
1562 NodeManagerScope
nms(d_nodeManager
);
1563 Trace("smt") << "SMT getStackLevel()" << endl
;
1564 return d_context
->getLevel();
1567 void SmtEngine::push() {
1568 NodeManagerScope
nms(d_nodeManager
);
1569 Trace("smt") << "SMT push()" << endl
;
1570 d_private
->processAssertions();
1571 if(Dump
.isOn("benchmark")) {
1572 Dump("benchmark") << PushCommand();
1574 if(!Options::current()->incrementalSolving
) {
1575 throw ModalException("Cannot push when not solving incrementally (use --incremental)");
1578 // check to see if a postsolve() is pending
1579 if(d_needPostsolve
) {
1580 d_theoryEngine
->postsolve();
1581 d_needPostsolve
= false;
1584 d_userLevels
.push_back(d_userContext
->getLevel());
1586 Trace("userpushpop") << "SmtEngine: pushed to level "
1587 << d_userContext
->getLevel() << endl
;
1590 void SmtEngine::pop() {
1591 NodeManagerScope
nms(d_nodeManager
);
1592 Trace("smt") << "SMT pop()" << endl
;
1593 if(Dump
.isOn("benchmark")) {
1594 Dump("benchmark") << PopCommand();
1596 if(!Options::current()->incrementalSolving
) {
1597 throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
1599 if(d_userContext
->getLevel() == 0) {
1600 throw ModalException("Cannot pop beyond the first user frame");
1603 // check to see if a postsolve() is pending
1604 if(d_needPostsolve
) {
1605 d_theoryEngine
->postsolve();
1606 d_needPostsolve
= false;
1609 AlwaysAssert(d_userLevels
.size() > 0 && d_userLevels
.back() < d_userContext
->getLevel());
1610 while (d_userLevels
.back() < d_userContext
->getLevel()) {
1613 d_userLevels
.pop_back();
1615 // Clear out assertion queues etc., in case anything is still in there
1616 d_private
->notifyPop();
1618 Trace("userpushpop") << "SmtEngine: popped to level "
1619 << d_userContext
->getLevel() << endl
;
1620 // FIXME: should we reset d_status here?
1621 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
1622 // Still, we want the right exit status after any final sequence
1626 void SmtEngine::internalPush() {
1627 Trace("smt") << "SmtEngine::internalPush()" << endl
;
1628 if(Options::current()->incrementalSolving
) {
1629 d_private
->processAssertions();
1630 d_userContext
->push();
1632 d_propEngine
->push();
1636 void SmtEngine::internalPop() {
1637 Trace("smt") << "SmtEngine::internalPop()" << endl
;
1638 if(Options::current()->incrementalSolving
) {
1639 d_propEngine
->pop();
1641 d_userContext
->pop();
1645 void SmtEngine::interrupt() throw(ModalException
) {
1646 d_propEngine
->interrupt();
1649 void SmtEngine::setResourceLimit(unsigned long units
, bool cumulative
) {
1651 Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units
<< endl
;
1652 d_resourceBudgetCumulative
= (units
== 0) ? 0 : (d_cumulativeResourceUsed
+ units
);
1654 Trace("limit") << "SmtEngine: setting per-call resource limit to " << units
<< endl
;
1655 d_resourceBudgetPerCall
= units
;
1659 void SmtEngine::setTimeLimit(unsigned long millis
, bool cumulative
) {
1661 Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis
<< " ms" << endl
;
1662 d_timeBudgetCumulative
= (millis
== 0) ? 0 : (d_cumulativeTimeUsed
+ millis
);
1664 Trace("limit") << "SmtEngine: setting per-call time limit to " << millis
<< " ms" << endl
;
1665 d_timeBudgetPerCall
= millis
;
1669 unsigned long SmtEngine::getResourceUsage() const {
1670 return d_cumulativeResourceUsed
;
1673 unsigned long SmtEngine::getTimeUsage() const {
1674 return d_cumulativeTimeUsed
;
1677 unsigned long SmtEngine::getResourceRemaining() const throw(ModalException
) {
1678 if(d_resourceBudgetCumulative
== 0) {
1679 throw ModalException("No cumulative resource limit is currently set");
1682 return d_resourceBudgetCumulative
<= d_cumulativeResourceUsed
? 0 :
1683 d_resourceBudgetCumulative
- d_cumulativeResourceUsed
;
1686 unsigned long SmtEngine::getTimeRemaining() const throw(ModalException
) {
1687 if(d_timeBudgetCumulative
== 0) {
1688 throw ModalException("No cumulative time limit is currently set");
1691 return d_timeBudgetCumulative
<= d_cumulativeTimeUsed
? 0 :
1692 d_timeBudgetCumulative
- d_cumulativeTimeUsed
;
1695 StatisticsRegistry
* SmtEngine::getStatisticsRegistry() const {
1696 return d_exprManager
->d_nodeManager
->getStatisticsRegistry();
1699 }/* CVC4 namespace */