1 /********************* */
2 /*! \file smt_engine.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: Clark Barrett
6 ** Minor contributors (to current version): Christopher L. Conway, Tianyi Liang, Martin Brain <>, Kshitij Bansal, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief The main entry point into the CVC4 library's SMT interface
14 ** 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 "decision/decision_mode.h"
32 #include "decision/options.h"
33 #include "expr/command.h"
34 #include "expr/expr.h"
35 #include "expr/kind.h"
36 #include "expr/metakind.h"
37 #include "expr/node_builder.h"
38 #include "expr/node.h"
39 #include "expr/node_self_iterator.h"
40 #include "prop/prop_engine.h"
41 #include "proof/theory_proof.h"
42 #include "smt/modal_exception.h"
43 #include "smt/smt_engine.h"
44 #include "smt/smt_engine_scope.h"
45 #include "smt/model_postprocessor.h"
46 #include "smt/logic_request.h"
47 #include "theory/theory_engine.h"
48 #include "theory/bv/theory_bv_rewriter.h"
49 #include "proof/proof_manager.h"
50 #include "main/options.h"
51 #include "util/unsat_core.h"
52 #include "util/proof.h"
53 #include "proof/proof.h"
54 #include "proof/proof_manager.h"
55 #include "util/boolean_simplification.h"
56 #include "util/node_visitor.h"
57 #include "util/configuration.h"
58 #include "util/exception.h"
59 #include "util/nary_builder.h"
60 #include "smt/command_list.h"
61 #include "smt/boolean_terms.h"
62 #include "smt/options.h"
63 #include "options/option_exception.h"
64 #include "util/output.h"
65 #include "util/hash.h"
66 #include "theory/substitutions.h"
67 #include "theory/uf/options.h"
68 #include "theory/arith/options.h"
69 #include "theory/strings/options.h"
70 #include "theory/bv/options.h"
71 #include "theory/theory_traits.h"
72 #include "theory/logic_info.h"
73 #include "theory/options.h"
74 #include "theory/booleans/circuit_propagator.h"
75 #include "theory/booleans/boolean_term_conversion_mode.h"
76 #include "theory/booleans/options.h"
77 #include "util/ite_removal.h"
78 #include "theory/theory_model.h"
79 #include "printer/printer.h"
80 #include "prop/options.h"
81 #include "theory/arrays/options.h"
82 #include "util/sort_inference.h"
83 #include "theory/quantifiers/quant_conflict_find.h"
84 #include "theory/quantifiers/macros.h"
85 #include "theory/quantifiers/first_order_reasoning.h"
86 #include "theory/quantifiers/quantifiers_rewriter.h"
87 #include "theory/quantifiers/options.h"
88 #include "theory/datatypes/options.h"
89 #include "theory/strings/theory_strings_preprocess.h"
90 #include "printer/options.h"
92 #include "theory/arith/pseudoboolean_proc.h"
93 #include "theory/bv/bvintropow2.h"
97 using namespace CVC4::smt
;
98 using namespace CVC4::prop
;
99 using namespace CVC4::context
;
100 using namespace CVC4::theory
;
106 /** Useful for counting the number of recursive calls. */
111 ScopeCounter(unsigned& d
) : d_depth(d
) {
120 * Representation of a defined function. We keep these around in
121 * SmtEngine to permit expanding definitions late (and lazily), to
122 * support getValue() over defined functions, to support user output
123 * in terms of defined functions, etc.
125 class DefinedFunction
{
127 vector
<Node
> d_formals
;
131 DefinedFunction(Node func
, vector
<Node
> formals
, Node formula
) :
136 Node
getFunction() const { return d_func
; }
137 vector
<Node
> getFormals() const { return d_formals
; }
138 Node
getFormula() const { return d_formula
; }
139 };/* class DefinedFunction */
141 class AssertionPipeline
{
142 vector
<Node
> d_nodes
;
146 size_t size() const { return d_nodes
.size(); }
148 void resize(size_t n
) { d_nodes
.resize(n
); }
149 void clear() { d_nodes
.clear(); }
151 Node
& operator[](size_t i
) { return d_nodes
[i
]; }
152 const Node
& operator[](size_t i
) const { return d_nodes
[i
]; }
153 void push_back(Node n
) { d_nodes
.push_back(n
); }
155 vector
<Node
>& ref() { return d_nodes
; }
156 const vector
<Node
>& ref() const { return d_nodes
; }
158 void replace(size_t i
, Node n
) {
159 PROOF( ProofManager::currentPM()->addDependence(n
, d_nodes
[i
]); );
163 };/* class AssertionPipeline */
165 struct SmtEngineStatistics
{
166 /** time spent in definition-expansion */
167 TimerStat d_definitionExpansionTime
;
168 /** time spent in Boolean term rewriting */
169 TimerStat d_rewriteBooleanTermsTime
;
170 /** time spent in non-clausal simplification */
171 TimerStat d_nonclausalSimplificationTime
;
172 /** time spent in miplib pass */
173 TimerStat d_miplibPassTime
;
174 /** number of assertions removed by miplib pass */
175 IntStat d_numMiplibAssertionsRemoved
;
176 /** number of constant propagations found during nonclausal simp */
177 IntStat d_numConstantProps
;
178 /** time spent in static learning */
179 TimerStat d_staticLearningTime
;
180 /** time spent in simplifying ITEs */
181 TimerStat d_simpITETime
;
182 /** time spent in simplifying ITEs */
183 TimerStat d_unconstrainedSimpTime
;
184 /** time spent removing ITEs */
185 TimerStat d_iteRemovalTime
;
186 /** time spent in theory preprocessing */
187 TimerStat d_theoryPreprocessTime
;
188 /** time spent in theory preprocessing */
189 TimerStat d_rewriteApplyToConstTime
;
190 /** time spent converting to CNF */
191 TimerStat d_cnfConversionTime
;
192 /** Num of assertions before ite removal */
193 IntStat d_numAssertionsPre
;
194 /** Num of assertions after ite removal */
195 IntStat d_numAssertionsPost
;
196 /** time spent in checkModel() */
197 TimerStat d_checkModelTime
;
198 /** time spent in checkProof() */
199 TimerStat d_checkProofTime
;
200 /** time spent in PropEngine::checkSat() */
201 TimerStat d_solveTime
;
202 /** time spent in pushing/popping */
203 TimerStat d_pushPopTime
;
204 /** time spent in processAssertions() */
205 TimerStat d_processAssertionsTime
;
207 /** Has something simplified to false? */
208 IntStat d_simplifiedToFalse
;
210 SmtEngineStatistics() :
211 d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
212 d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"),
213 d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
214 d_miplibPassTime("smt::SmtEngine::miplibPassTime"),
215 d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0),
216 d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
217 d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
218 d_simpITETime("smt::SmtEngine::simpITETime"),
219 d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
220 d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
221 d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
222 d_rewriteApplyToConstTime("smt::SmtEngine::rewriteApplyToConstTime"),
223 d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
224 d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
225 d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
226 d_checkModelTime("smt::SmtEngine::checkModelTime"),
227 d_checkProofTime("smt::SmtEngine::checkProofTime"),
228 d_solveTime("smt::SmtEngine::solveTime"),
229 d_pushPopTime("smt::SmtEngine::pushPopTime"),
230 d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
231 d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
234 StatisticsRegistry::registerStat(&d_definitionExpansionTime
);
235 StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime
);
236 StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime
);
237 StatisticsRegistry::registerStat(&d_miplibPassTime
);
238 StatisticsRegistry::registerStat(&d_numMiplibAssertionsRemoved
);
239 StatisticsRegistry::registerStat(&d_numConstantProps
);
240 StatisticsRegistry::registerStat(&d_staticLearningTime
);
241 StatisticsRegistry::registerStat(&d_simpITETime
);
242 StatisticsRegistry::registerStat(&d_unconstrainedSimpTime
);
243 StatisticsRegistry::registerStat(&d_iteRemovalTime
);
244 StatisticsRegistry::registerStat(&d_theoryPreprocessTime
);
245 StatisticsRegistry::registerStat(&d_rewriteApplyToConstTime
);
246 StatisticsRegistry::registerStat(&d_cnfConversionTime
);
247 StatisticsRegistry::registerStat(&d_numAssertionsPre
);
248 StatisticsRegistry::registerStat(&d_numAssertionsPost
);
249 StatisticsRegistry::registerStat(&d_checkModelTime
);
250 StatisticsRegistry::registerStat(&d_checkProofTime
);
251 StatisticsRegistry::registerStat(&d_solveTime
);
252 StatisticsRegistry::registerStat(&d_pushPopTime
);
253 StatisticsRegistry::registerStat(&d_processAssertionsTime
);
254 StatisticsRegistry::registerStat(&d_simplifiedToFalse
);
257 ~SmtEngineStatistics() {
258 StatisticsRegistry::unregisterStat(&d_definitionExpansionTime
);
259 StatisticsRegistry::unregisterStat(&d_rewriteBooleanTermsTime
);
260 StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime
);
261 StatisticsRegistry::unregisterStat(&d_miplibPassTime
);
262 StatisticsRegistry::unregisterStat(&d_numMiplibAssertionsRemoved
);
263 StatisticsRegistry::unregisterStat(&d_numConstantProps
);
264 StatisticsRegistry::unregisterStat(&d_staticLearningTime
);
265 StatisticsRegistry::unregisterStat(&d_simpITETime
);
266 StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime
);
267 StatisticsRegistry::unregisterStat(&d_iteRemovalTime
);
268 StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime
);
269 StatisticsRegistry::unregisterStat(&d_rewriteApplyToConstTime
);
270 StatisticsRegistry::unregisterStat(&d_cnfConversionTime
);
271 StatisticsRegistry::unregisterStat(&d_numAssertionsPre
);
272 StatisticsRegistry::unregisterStat(&d_numAssertionsPost
);
273 StatisticsRegistry::unregisterStat(&d_checkModelTime
);
274 StatisticsRegistry::unregisterStat(&d_checkProofTime
);
275 StatisticsRegistry::unregisterStat(&d_solveTime
);
276 StatisticsRegistry::unregisterStat(&d_pushPopTime
);
277 StatisticsRegistry::unregisterStat(&d_processAssertionsTime
);
278 StatisticsRegistry::unregisterStat(&d_simplifiedToFalse
);
280 };/* struct SmtEngineStatistics */
283 * This is an inelegant solution, but for the present, it will work.
284 * The point of this is to separate the public and private portions of
285 * the SmtEngine class, so that smt_engine.h doesn't
286 * include "expr/node.h", which is a private CVC4 header (and can lead
287 * to linking errors due to the improper inlining of non-visible symbols
290 * The "real" solution (that which is usually implemented) is to move
291 * ALL the implementation to SmtEnginePrivate and maintain a
292 * heap-allocated instance of it in SmtEngine. SmtEngine (the public
293 * one) becomes an "interface shell" which simply acts as a forwarder
296 class SmtEnginePrivate
: public NodeManagerListener
{
299 /** Learned literals */
300 vector
<Node
> d_nonClausalLearnedLiterals
;
302 /** Size of assertions array when preprocessing starts */
303 unsigned d_realAssertionsEnd
;
305 /** The converter for Boolean terms -> BITVECTOR(1). */
306 BooleanTermConverter
* d_booleanTermConverter
;
308 /** A circuit propagator for non-clausal propositional deduction */
309 booleans::CircuitPropagator d_propagator
;
310 bool d_propagatorNeedsFinish
;
311 std::vector
<Node
> d_boolVars
;
313 /** Assertions in the preprocessing pipeline */
314 AssertionPipeline d_assertions
;
316 /** Whether any assertions have been processed */
317 CDO
<bool> d_assertionsProcessed
;
319 /** Index for where to store substitutions */
320 CDO
<unsigned> d_substitutionsIndex
;
326 * A context that never pushes/pops, for use by CD structures (like
327 * SubstitutionMaps) that should be "global".
329 context::Context d_fakeContext
;
332 * A map of AbsractValues to their actual constants. Only used if
333 * options::abstractValues() is on.
335 SubstitutionMap d_abstractValueMap
;
338 * A mapping of all abstract values (actual value |-> abstract) that
339 * we've handed out. This is necessary to ensure that we give the
340 * same AbstractValues for the same real constants. Only used if
341 * options::abstractValues() is on.
343 hash_map
<Node
, Node
, NodeHashFunction
> d_abstractValues
;
345 /** Number of calls of simplify assertions active.
347 unsigned d_simplifyAssertionsDepth
;
351 * Map from skolem variables to index in d_assertions containing
352 * corresponding introduced Boolean ite
354 IteSkolemMap d_iteSkolemMap
;
356 /** Instance of the ITE remover */
357 RemoveITE d_iteRemover
;
361 theory::arith::PseudoBooleanProcessor d_pbsProcessor
;
363 /** The top level substitutions */
364 SubstitutionMap d_topLevelSubstitutions
;
366 static const bool d_doConstantProp
= true;
369 * Runs the nonclausal solver and tries to solve all the assigned
372 * Returns false if the formula simplifies to "false"
374 bool nonClausalSimplify();
377 * Performs static learning on the assertions.
379 void staticLearning();
382 * Remove ITEs from the assertions.
387 * Helper function to fix up assertion list to restore invariants needed after ite removal
389 void collectSkolems(TNode n
, set
<TNode
>& skolemSet
, hash_map
<Node
, bool, NodeHashFunction
>& cache
);
392 * Helper function to fix up assertion list to restore invariants needed after ite removal
394 bool checkForBadSkolems(TNode n
, TNode skolem
, hash_map
<Node
, bool, NodeHashFunction
>& cache
);
396 // Lift bit-vectors of size 1 to booleans
399 // Abstract common structure over small domains to UF
400 // return true if changes were made.
401 void bvAbstraction();
403 // Simplify ITE structure
406 // Simplify based on unconstrained values
407 void unconstrainedSimp();
409 // Ensures the assertions asserted after before now
410 // effectively come before d_realAssertionsEnd
411 void compressBeforeRealAssertions(size_t before
);
414 * Any variable in an assertion that is declared as a subtype type
415 * (predicate subtype or integer subrange type) must be constrained
416 * to be in that type.
418 void constrainSubtypes(TNode n
, AssertionPipeline
& assertions
)
421 // trace nodes back to their assertions using CircuitPropagator's BackEdgesMap
422 void traceBackToAssertions(const std::vector
<Node
>& nodes
, std::vector
<TNode
>& assertions
);
423 // remove conjuncts in toRemove from conjunction n; return # of removed conjuncts
424 size_t removeFromConjunction(Node
& n
, const std::hash_set
<unsigned long>& toRemove
);
426 // scrub miplib encodings
427 void doMiplibTrick();
430 * Perform non-clausal simplification of a Node. This involves
431 * Theory implementations, but does NOT involve the SAT solver in
434 * Returns false if the formula simplifies to "false"
436 bool simplifyAssertions() throw(TypeCheckingException
, LogicException
);
440 SmtEnginePrivate(SmtEngine
& smt
) :
442 d_nonClausalLearnedLiterals(),
443 d_realAssertionsEnd(0),
444 d_booleanTermConverter(NULL
),
445 d_propagator(d_nonClausalLearnedLiterals
, true, true),
446 d_propagatorNeedsFinish(false),
448 d_assertionsProcessed(smt
.d_userContext
, false),
449 d_substitutionsIndex(smt
.d_userContext
, 0),
451 d_abstractValueMap(&d_fakeContext
),
453 d_simplifyAssertionsDepth(0),
455 d_iteRemover(smt
.d_userContext
),
456 d_pbsProcessor(smt
.d_userContext
),
457 d_topLevelSubstitutions(smt
.d_userContext
)
459 d_smt
.d_nodeManager
->subscribeEvents(this);
460 d_true
= NodeManager::currentNM()->mkConst(true);
463 ~SmtEnginePrivate() {
464 if(d_propagatorNeedsFinish
) {
465 d_propagator
.finish();
466 d_propagatorNeedsFinish
= false;
468 if(d_booleanTermConverter
!= NULL
) {
469 delete d_booleanTermConverter
;
470 d_booleanTermConverter
= NULL
;
472 d_smt
.d_nodeManager
->unsubscribeEvents(this);
475 void nmNotifyNewSort(TypeNode tn
, uint32_t flags
) {
476 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
479 if((flags
& ExprManager::SORT_FLAG_PLACEHOLDER
) == 0) {
480 d_smt
.addToModelCommandAndDump(c
, flags
);
484 void nmNotifyNewSortConstructor(TypeNode tn
) {
485 DeclareTypeCommand
c(tn
.getAttribute(expr::VarNameAttr()),
486 tn
.getAttribute(expr::SortArityAttr()),
488 d_smt
.addToModelCommandAndDump(c
);
491 void nmNotifyNewDatatypes(const std::vector
<DatatypeType
>& dtts
) {
492 DatatypeDeclarationCommand
c(dtts
);
493 d_smt
.addToModelCommandAndDump(c
);
496 void nmNotifyNewVar(TNode n
, uint32_t flags
) {
497 DeclareFunctionCommand
c(n
.getAttribute(expr::VarNameAttr()),
499 n
.getType().toType());
500 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
501 d_smt
.addToModelCommandAndDump(c
, flags
);
503 if(n
.getType().isBoolean() && !options::incrementalSolving()) {
504 d_boolVars
.push_back(n
);
508 void nmNotifyNewSkolem(TNode n
, const std::string
& comment
, uint32_t flags
) {
509 string id
= n
.getAttribute(expr::VarNameAttr());
510 DeclareFunctionCommand
c(id
,
512 n
.getType().toType());
513 if(Dump
.isOn("skolems") && comment
!= "") {
514 Dump("skolems") << CommentCommand(id
+ " is " + comment
);
516 if((flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
517 d_smt
.addToModelCommandAndDump(c
, flags
, false, "skolems");
519 if(n
.getType().isBoolean() && !options::incrementalSolving()) {
520 d_boolVars
.push_back(n
);
524 Node
applySubstitutions(TNode node
) const {
525 return Rewriter::rewrite(d_topLevelSubstitutions
.apply(node
));
529 * Process the assertions that have been asserted.
531 void processAssertions();
534 * Process a user pop. Clears out the non-context-dependent stuff in this
535 * SmtEnginePrivate. Necessary to clear out our assertion vectors in case
536 * someone does a push-assert-pop without a check-sat.
539 d_assertions
.clear();
540 d_nonClausalLearnedLiterals
.clear();
541 d_realAssertionsEnd
= 0;
542 d_iteSkolemMap
.clear();
546 * Adds a formula to the current context. Action here depends on
547 * the SimplificationMode (in the current Options scope); the
548 * formula might be pushed out to the propositional layer
549 * immediately, or it might be simplified and kept, or it might not
550 * even be simplified.
552 void addFormula(TNode n
)
553 throw(TypeCheckingException
, LogicException
);
556 * Expand definitions in n.
558 Node
expandDefinitions(TNode n
, hash_map
<Node
, Node
, NodeHashFunction
>& cache
, bool expandOnly
= false)
559 throw(TypeCheckingException
, LogicException
);
562 * Rewrite Boolean terms in a Node.
564 Node
rewriteBooleanTerms(TNode n
);
567 * Simplify node "in" by expanding definitions and applying any
568 * substitutions learned from preprocessing.
570 Node
simplify(TNode in
) {
571 // Substitute out any abstract values in ex.
572 // Expand definitions.
573 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
574 Node n
= expandDefinitions(in
, cache
).toExpr();
575 // Make sure we've done all preprocessing, etc.
576 Assert(d_assertions
.size() == 0);
577 return applySubstitutions(n
).toExpr();
581 * Substitute away all AbstractValues in a node.
583 Node
substituteAbstractValues(TNode n
) {
584 // We need to do this even if options::abstractValues() is off,
585 // since the setting might have changed after we already gave out
586 // some abstract values.
587 return d_abstractValueMap
.apply(n
);
591 * Make a new (or return an existing) abstract value for a node.
592 * Can only use this if options::abstractValues() is on.
594 Node
mkAbstractValue(TNode n
) {
595 Assert(options::abstractValues());
596 Node
& val
= d_abstractValues
[n
];
598 val
= d_smt
.d_nodeManager
->mkAbstractValue(n
.getType());
599 d_abstractValueMap
.addSubstitution(val
, n
);
604 std::hash_map
<Node
, Node
, NodeHashFunction
> rewriteApplyToConstCache
;
605 Node
rewriteApplyToConst(TNode n
) {
606 Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n
<< std::endl
;
608 if(n
.getMetaKind() == kind::metakind::CONSTANT
|| n
.getMetaKind() == kind::metakind::VARIABLE
) {
612 if(rewriteApplyToConstCache
.find(n
) != rewriteApplyToConstCache
.end()) {
613 Trace("rewriteApplyToConst") << "in cache :: " << rewriteApplyToConstCache
[n
] << std::endl
;
614 return rewriteApplyToConstCache
[n
];
616 if(n
.getKind() == kind::APPLY_UF
) {
617 if(n
.getNumChildren() == 1 && n
[0].isConst() && n
[0].getType().isInteger()) {
619 ss
<< n
.getOperator() << "_";
620 if(n
[0].getConst
<Rational
>() < 0) {
621 ss
<< "m" << -n
[0].getConst
<Rational
>();
625 Node newvar
= NodeManager::currentNM()->mkSkolem(ss
.str(), n
.getType(), "rewriteApplyToConst skolem", NodeManager::SKOLEM_EXACT_NAME
);
626 rewriteApplyToConstCache
[n
] = newvar
;
627 Trace("rewriteApplyToConst") << "made :: " << newvar
<< std::endl
;
631 ss
<< "The rewrite-apply-to-const preprocessor is currently limited;\n"
632 << "it only works if all function symbols are unary and with Integer\n"
633 << "domain, and all applications are to integer values.\n"
634 << "Found application: " << n
;
639 NodeBuilder
<> builder(n
.getKind());
640 if(n
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
641 builder
<< n
.getOperator();
643 for(unsigned i
= 0; i
< n
.getNumChildren(); ++i
) {
644 builder
<< rewriteApplyToConst(n
[i
]);
647 rewriteApplyToConstCache
[n
] = rewr
;
648 Trace("rewriteApplyToConst") << "built :: " << rewr
<< std::endl
;
652 };/* class SmtEnginePrivate */
654 }/* namespace CVC4::smt */
656 SmtEngine::SmtEngine(ExprManager
* em
) throw() :
657 d_context(em
->getContext()),
659 d_userContext(new UserContext()),
661 d_nodeManager(d_exprManager
->getNodeManager()),
662 d_decisionEngine(NULL
),
663 d_theoryEngine(NULL
),
665 d_proofManager(NULL
),
666 d_definedFunctions(NULL
),
667 d_assertionList(NULL
),
669 d_modelGlobalCommands(),
670 d_modelCommands(NULL
),
674 d_fullyInited(false),
675 d_problemExtended(false),
677 d_needPostsolve(false),
678 d_earlyTheoryPP(true),
679 d_timeBudgetCumulative(0),
680 d_timeBudgetPerCall(0),
681 d_resourceBudgetCumulative(0),
682 d_resourceBudgetPerCall(0),
683 d_cumulativeTimeUsed(0),
684 d_cumulativeResourceUsed(0),
687 d_statisticsRegistry(NULL
),
691 d_private
= new smt::SmtEnginePrivate(*this);
692 d_statisticsRegistry
= new StatisticsRegistry();
693 d_stats
= new SmtEngineStatistics();
695 // We have mutual dependency here, so we add the prop engine to the theory
696 // engine later (it is non-essential there)
697 d_theoryEngine
= new TheoryEngine(d_context
, d_userContext
, d_private
->d_iteRemover
, const_cast<const LogicInfo
&>(d_logic
));
700 for(TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
701 TheoryConstructor::addTheory(d_theoryEngine
, id
);
704 // global push/pop around everything, to ensure proper destruction
705 // of context-dependent data structures
706 d_userContext
->push();
709 d_definedFunctions
= new(true) DefinedFunctionMap(d_userContext
);
710 d_modelCommands
= new(true) smt::CommandList(d_userContext
);
713 void SmtEngine::finishInit() {
714 // ensure that our heuristics are properly set up
717 Assert(d_proofManager
== NULL
);
718 PROOF( d_proofManager
= new ProofManager(); );
720 d_decisionEngine
= new DecisionEngine(d_context
, d_userContext
);
721 d_decisionEngine
->init(); // enable appropriate strategies
723 d_propEngine
= new PropEngine(d_theoryEngine
, d_decisionEngine
, d_context
, d_userContext
);
725 d_theoryEngine
->setPropEngine(d_propEngine
);
726 d_theoryEngine
->setDecisionEngine(d_decisionEngine
);
727 d_theoryEngine
->finishInit();
729 // [MGD 10/20/2011] keep around in incremental mode, due to a
730 // cleanup ordering issue and Nodes/TNodes. If SAT is popped
731 // first, some user-context-dependent TNodes might still exist
733 if(options::interactive() ||
734 options::incrementalSolving()) {
735 // In the case of incremental solving, we appear to need these to
736 // ensure the relevant Nodes remain live.
737 d_assertionList
= new(true) AssertionList(d_userContext
);
740 // dump out a set-logic command
741 if(Dump
.isOn("benchmark")) {
742 // Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
743 LogicInfo everything
;
745 Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, \"all-supported\" logic (below), as some internals might require the use of a logic more general than the input.")
746 << SetBenchmarkLogicCommand(everything
.getLogicString());
749 // dump out any pending declaration commands
750 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
751 Dump("declarations") << *d_dumpCommands
[i
];
752 delete d_dumpCommands
[i
];
754 d_dumpCommands
.clear();
756 if(options::perCallResourceLimit() != 0) {
757 setResourceLimit(options::perCallResourceLimit(), false);
759 if(options::cumulativeResourceLimit() != 0) {
760 setResourceLimit(options::cumulativeResourceLimit(), true);
762 if(options::perCallMillisecondLimit() != 0) {
763 setTimeLimit(options::perCallMillisecondLimit(), false);
765 if(options::cumulativeMillisecondLimit() != 0) {
766 setTimeLimit(options::cumulativeMillisecondLimit(), true);
769 PROOF( ProofManager::currentPM()->setLogic(d_logic
.getLogicString()); );
772 void SmtEngine::finalOptionsAreSet() {
777 if(! d_logic
.isLocked()) {
781 // finish initialization, create the prop engine, etc.
784 AlwaysAssert( d_propEngine
->getAssertionLevel() == 0,
785 "The PropEngine has pushed but the SmtEngine "
786 "hasn't finished initializing!" );
788 d_fullyInited
= true;
789 Assert(d_logic
.isLocked());
791 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(true));
792 d_propEngine
->assertFormula(NodeManager::currentNM()->mkConst
<bool>(false).notNode());
795 void SmtEngine::shutdown() {
798 while(options::incrementalSolving() && d_userContext
->getLevel() > 1) {
802 // check to see if a postsolve() is pending
803 if(d_needPostsolve
) {
804 d_theoryEngine
->postsolve();
805 d_needPostsolve
= false;
808 if(d_propEngine
!= NULL
) {
809 d_propEngine
->shutdown();
811 if(d_theoryEngine
!= NULL
) {
812 d_theoryEngine
->shutdown();
814 if(d_decisionEngine
!= NULL
) {
815 d_decisionEngine
->shutdown();
819 SmtEngine::~SmtEngine() throw() {
825 // global push/pop around everything, to ensure proper destruction
826 // of context-dependent data structures
828 d_userContext
->popto(0);
830 if(d_assignments
!= NULL
) {
831 d_assignments
->deleteSelf();
834 if(d_assertionList
!= NULL
) {
835 d_assertionList
->deleteSelf();
838 for(unsigned i
= 0; i
< d_dumpCommands
.size(); ++i
) {
839 delete d_dumpCommands
[i
];
841 d_dumpCommands
.clear();
843 if(d_modelCommands
!= NULL
) {
844 d_modelCommands
->deleteSelf();
847 d_definedFunctions
->deleteSelf();
849 delete d_theoryEngine
;
851 delete d_decisionEngine
;
854 delete d_statisticsRegistry
;
858 delete d_userContext
;
860 } catch(Exception
& e
) {
861 Warning() << "CVC4 threw an exception during cleanup." << endl
866 void SmtEngine::setLogic(const LogicInfo
& logic
) throw(ModalException
) {
869 throw ModalException("Cannot set logic in SmtEngine after the engine has finished initializing");
875 void SmtEngine::setLogic(const std::string
& s
) throw(ModalException
, LogicException
) {
878 setLogic(LogicInfo(s
));
879 } catch(IllegalArgumentException
& e
) {
880 throw LogicException(e
.what());
884 void SmtEngine::setLogic(const char* logic
) throw(ModalException
, LogicException
) {
885 setLogic(string(logic
));
888 LogicInfo
SmtEngine::getLogicInfo() const {
892 void SmtEngine::setLogicInternal() throw() {
893 Assert(!d_fullyInited
, "setting logic in SmtEngine but the engine has already finished initializing for this run");
897 void SmtEngine::setDefaults() {
898 if(options::forceLogic
.wasSetByUser()) {
899 d_logic
= options::forceLogic();
903 /* - disabled for 1.4 release [MGD 2014.06.25]
904 if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
905 if(! options::stringExp.wasSetByUser()) {
906 options::stringExp.set( true );
907 Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
912 if(options::stringExp()) {
913 if( !d_logic
.isQuantified() ) {
914 d_logic
= d_logic
.getUnlockedCopy();
915 d_logic
.enableQuantifiers();
917 Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl
;
919 if(! options::finiteModelFind
.wasSetByUser()) {
920 options::finiteModelFind
.set( true );
921 Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl
;
923 if(! options::fmfBoundInt
.wasSetByUser()) {
924 if(! options::fmfBoundIntLazy
.wasSetByUser()) {
925 options::fmfBoundIntLazy
.set( true );
927 options::fmfBoundInt
.set( true );
928 Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl
;
931 if(! options::rewriteDivk.wasSetByUser()) {
932 options::rewriteDivk.set( true );
933 Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
936 if(! options::stringFMF.wasSetByUser()) {
937 options::stringFMF.set( true );
938 Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
943 if(options::checkModels()) {
944 if(! options::interactive()) {
945 Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl
;
946 setOption("interactive-mode", SExpr("true"));
950 if(options::unsatCores()) {
951 if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
952 if(options::simplificationMode
.wasSetByUser()) {
953 throw OptionException("simplification not supported with unsat cores");
955 Notice() << "SmtEngine: turning off simplification to support unsat-cores" << endl
;
956 options::simplificationMode
.set(SIMPLIFICATION_MODE_NONE
);
959 if(options::unconstrainedSimp()) {
960 if(options::unconstrainedSimp
.wasSetByUser()) {
961 throw OptionException("unconstrained simplification not supported with unsat cores");
963 Notice() << "SmtEngine: turning off unconstrained simplification to support unsat-cores" << endl
;
964 options::unconstrainedSimp
.set(false);
967 if(options::pbRewrites()) {
968 if(options::pbRewrites
.wasSetByUser()) {
969 throw OptionException("pseudoboolean rewrites not supported with unsat cores");
971 Notice() << "SmtEngine: turning off pseudoboolean rewrites to support unsat-cores" << endl
;
972 setOption("pb-rewrites", false);
975 if(options::sortInference()) {
976 if(options::sortInference
.wasSetByUser()) {
977 throw OptionException("sort inference not supported with unsat cores");
979 Notice() << "SmtEngine: turning off sort inference to support unsat-cores" << endl
;
980 options::sortInference
.set(false);
983 if(options::preSkolemQuant()) {
984 if(options::preSkolemQuant
.wasSetByUser()) {
985 throw OptionException("pre-skolemization not supported with unsat cores");
987 Notice() << "SmtEngine: turning off pre-skolemization to support unsat-cores" << endl
;
988 options::preSkolemQuant
.set(false);
991 if(options::bitvectorToBool()) {
992 if(options::bitvectorToBool
.wasSetByUser()) {
993 throw OptionException("bv-to-bool not supported with unsat cores");
995 Notice() << "SmtEngine: turning off bitvector-to-bool support unsat-cores" << endl
;
996 options::bitvectorToBool
.set(false);
999 if(options::bvIntroducePow2()) {
1000 if(options::bvIntroducePow2
.wasSetByUser()) {
1001 throw OptionException("bv-intro-pow2 not supported with unsat cores");
1003 Notice() << "SmtEngine: turning off bv-introduce-pow2 to support unsat-cores" << endl
;
1004 setOption("bv-intro-pow2", false);
1008 if(options::produceAssignments() && !options::produceModels()) {
1009 Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl
;
1010 setOption("produce-models", SExpr("true"));
1013 // Set the options for the theoryOf
1014 if(!options::theoryOfMode
.wasSetByUser()) {
1015 if(d_logic
.isSharingEnabled() && !d_logic
.isTheoryEnabled(THEORY_BV
) && !d_logic
.isTheoryEnabled(THEORY_STRINGS
)) {
1016 Trace("smt") << "setting theoryof-mode to term-based" << endl
;
1017 options::theoryOfMode
.set(THEORY_OF_TERM_BASED
);
1021 // by default, symmetry breaker is on only for QF_UF
1022 if(! options::ufSymmetryBreaker
.wasSetByUser()) {
1023 bool qf_uf
= d_logic
.isPure(THEORY_UF
) && !d_logic
.isQuantified();
1024 Trace("smt") << "setting uf symmetry breaker to " << qf_uf
<< endl
;
1025 options::ufSymmetryBreaker
.set(qf_uf
);
1027 // by default, nonclausal simplification is off for QF_SAT
1028 if(! options::simplificationMode
.wasSetByUser()) {
1029 bool qf_sat
= d_logic
.isPure(THEORY_BOOL
) && !d_logic
.isQuantified();
1030 Trace("smt") << "setting simplification mode to <" << d_logic
.getLogicString() << "> " << (!qf_sat
) << endl
;
1031 //simplification=none works better for SMT LIB benchmarks with quantifiers, not others
1032 //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
1033 options::simplificationMode
.set(qf_sat
? SIMPLIFICATION_MODE_NONE
: SIMPLIFICATION_MODE_BATCH
);
1036 // If in arrays, set the UF handler to arrays
1037 if(d_logic
.isTheoryEnabled(THEORY_ARRAY
) && ( !d_logic
.isQuantified() ||
1038 (d_logic
.isQuantified() && !d_logic
.isTheoryEnabled(THEORY_UF
)))) {
1039 Theory::setUninterpretedSortOwner(THEORY_ARRAY
);
1041 Theory::setUninterpretedSortOwner(THEORY_UF
);
1043 // Turn on ite simplification for QF_LIA and QF_AUFBV
1044 if(! options::doITESimp
.wasSetByUser()) {
1045 bool qf_aufbv
= !d_logic
.isQuantified() &&
1046 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1047 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1048 d_logic
.isTheoryEnabled(THEORY_BV
);
1049 bool qf_lia
= !d_logic
.isQuantified() &&
1050 d_logic
.isPure(THEORY_ARITH
) &&
1051 d_logic
.isLinear() &&
1052 !d_logic
.isDifferenceLogic() &&
1053 !d_logic
.areRealsUsed();
1055 bool iteSimp
= (qf_aufbv
|| qf_lia
);
1056 Trace("smt") << "setting ite simplification to " << iteSimp
<< endl
;
1057 options::doITESimp
.set(iteSimp
);
1059 if(! options::compressItes
.wasSetByUser() ){
1060 bool qf_lia
= !d_logic
.isQuantified() &&
1061 d_logic
.isPure(THEORY_ARITH
) &&
1062 d_logic
.isLinear() &&
1063 !d_logic
.isDifferenceLogic() &&
1064 !d_logic
.areRealsUsed();
1066 bool compressIte
= qf_lia
;
1067 Trace("smt") << "setting ite compression to " << compressIte
<< endl
;
1068 options::compressItes
.set(compressIte
);
1070 if(! options::simplifyWithCareEnabled
.wasSetByUser() ){
1071 bool qf_aufbv
= !d_logic
.isQuantified() &&
1072 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1073 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1074 d_logic
.isTheoryEnabled(THEORY_BV
);
1076 bool withCare
= qf_aufbv
;
1077 Trace("smt") << "setting ite simplify with care to " << withCare
<< endl
;
1078 options::simplifyWithCareEnabled
.set(withCare
);
1080 // Turn off array eager index splitting for QF_AUFLIA
1081 if(! options::arraysEagerIndexSplitting
.wasSetByUser()) {
1082 if (not d_logic
.isQuantified() &&
1083 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1084 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1085 d_logic
.isTheoryEnabled(THEORY_ARITH
)) {
1086 Trace("smt") << "setting array eager index splitting to false" << endl
;
1087 options::arraysEagerIndexSplitting
.set(false);
1090 // Turn on model-based arrays for QF_AX (unless models are enabled)
1091 // if(! options::arraysModelBased.wasSetByUser()) {
1092 // if (not d_logic.isQuantified() &&
1093 // d_logic.isTheoryEnabled(THEORY_ARRAY) &&
1094 // d_logic.isPure(THEORY_ARRAY) &&
1095 // !options::produceModels() &&
1096 // !options::checkModels()) {
1097 // Trace("smt") << "turning on model-based array solver" << endl;
1098 // options::arraysModelBased.set(true);
1101 // Turn on multiple-pass non-clausal simplification for QF_AUFBV
1102 if(! options::repeatSimp
.wasSetByUser()) {
1103 bool repeatSimp
= !d_logic
.isQuantified() &&
1104 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) && d_logic
.isTheoryEnabled(THEORY_UF
) && d_logic
.isTheoryEnabled(THEORY_BV
));
1105 Trace("smt") << "setting repeat simplification to " << repeatSimp
<< endl
;
1106 options::repeatSimp
.set(repeatSimp
);
1108 // Turn on unconstrained simplification for QF_AUFBV
1109 if(! options::unconstrainedSimp
.wasSetByUser() || options::incrementalSolving()) {
1110 // bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
1111 // bool uncSimp = false && !qf_sat && !options::incrementalSolving();
1112 bool uncSimp
= !options::incrementalSolving() && !d_logic
.isQuantified() && !options::produceModels() && !options::produceAssignments() && !options::checkModels() &&
1113 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) && d_logic
.isTheoryEnabled(THEORY_BV
));
1114 Trace("smt") << "setting unconstrained simplification to " << uncSimp
<< endl
;
1115 options::unconstrainedSimp
.set(uncSimp
);
1117 // Unconstrained simp currently does *not* support model generation
1118 if (options::unconstrainedSimp
.wasSetByUser() && options::unconstrainedSimp()) {
1119 if (options::produceModels()) {
1120 if (options::produceModels
.wasSetByUser()) {
1121 throw OptionException("Cannot use unconstrained-simp with model generation.");
1123 Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl
;
1124 setOption("produce-models", SExpr("false"));
1126 if (options::produceAssignments()) {
1127 if (options::produceAssignments
.wasSetByUser()) {
1128 throw OptionException("Cannot use unconstrained-simp with model generation (produce-assignments).");
1130 Notice() << "SmtEngine: turning off produce-assignments to support unconstrainedSimp" << endl
;
1131 setOption("produce-assignments", SExpr("false"));
1133 if (options::checkModels()) {
1134 if (options::checkModels
.wasSetByUser()) {
1135 throw OptionException("Cannot use unconstrained-simp with model generation (check-models).");
1137 Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl
;
1138 setOption("check-models", SExpr("false"));
1143 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
1144 options::incrementalSolving()) {
1145 if (options::incrementalSolving
.wasSetByUser()) {
1146 throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\
1147 Try --bitblast=lazy"));
1149 Notice() << "SmtEngine: turning off incremental to support eager bit-blasting" << endl
;
1150 setOption("incremental", SExpr("false"));
1153 if (! options::bvEagerExplanations
.wasSetByUser() &&
1154 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1155 d_logic
.isTheoryEnabled(THEORY_BV
)) {
1156 Trace("smt") << "enabling eager bit-vector explanations " << endl
;
1157 options::bvEagerExplanations
.set(true);
1160 // Turn on arith rewrite equalities only for pure arithmetic
1161 if(! options::arithRewriteEq
.wasSetByUser()) {
1162 bool arithRewriteEq
= d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified();
1163 Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
<< endl
;
1164 options::arithRewriteEq
.set(arithRewriteEq
);
1166 if(! options::arithHeuristicPivots
.wasSetByUser()) {
1167 int16_t heuristicPivots
= 5;
1168 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()) {
1169 if(d_logic
.isDifferenceLogic()) {
1170 heuristicPivots
= -1;
1171 } else if(!d_logic
.areIntegersUsed()) {
1172 heuristicPivots
= 0;
1175 Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots
<< endl
;
1176 options::arithHeuristicPivots
.set(heuristicPivots
);
1178 if(! options::arithPivotThreshold
.wasSetByUser()){
1179 uint16_t pivotThreshold
= 2;
1180 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1181 if(d_logic
.isDifferenceLogic()){
1182 pivotThreshold
= 16;
1185 Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold
<< endl
;
1186 options::arithPivotThreshold
.set(pivotThreshold
);
1188 if(! options::arithStandardCheckVarOrderPivots
.wasSetByUser()){
1189 int16_t varOrderPivots
= -1;
1190 if(d_logic
.isPure(THEORY_ARITH
) && !d_logic
.isQuantified()){
1191 varOrderPivots
= 200;
1193 Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots
<< endl
;
1194 options::arithStandardCheckVarOrderPivots
.set(varOrderPivots
);
1196 // Turn off early theory preprocessing if arithRewriteEq is on
1197 if (options::arithRewriteEq()) {
1198 d_earlyTheoryPP
= false;
1201 // Set decision mode based on logic (if not set by user)
1202 if(!options::decisionMode
.wasSetByUser()) {
1203 decision::DecisionMode decMode
=
1205 d_logic
.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION
:
1207 (not d_logic
.isQuantified() &&
1208 d_logic
.isPure(THEORY_BV
)
1210 // QF_AUFBV or QF_ABV or QF_UFBV
1211 (not d_logic
.isQuantified() &&
1212 (d_logic
.isTheoryEnabled(THEORY_ARRAY
) ||
1213 d_logic
.isTheoryEnabled(THEORY_UF
)) &&
1214 d_logic
.isTheoryEnabled(THEORY_BV
)
1216 // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
1217 (not d_logic
.isQuantified() &&
1218 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1219 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1220 d_logic
.isTheoryEnabled(THEORY_ARITH
)
1223 (not d_logic
.isQuantified() &&
1224 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
1227 d_logic
.isQuantified() ||
1229 d_logic
.isTheoryEnabled(THEORY_STRINGS
)
1230 ? decision::DECISION_STRATEGY_JUSTIFICATION
1231 : decision::DECISION_STRATEGY_INTERNAL
1236 d_logic
.hasEverything() || d_logic
.isTheoryEnabled(THEORY_STRINGS
) ? false :
1238 (not d_logic
.isQuantified() &&
1239 d_logic
.isTheoryEnabled(THEORY_ARRAY
) &&
1240 d_logic
.isTheoryEnabled(THEORY_UF
) &&
1241 d_logic
.isTheoryEnabled(THEORY_ARITH
)
1244 (not d_logic
.isQuantified() &&
1245 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
1250 Trace("smt") << "setting decision mode to " << decMode
<< endl
;
1251 options::decisionMode
.set(decMode
);
1252 options::decisionStopOnly
.set(stoponly
);
1255 //for finite model finding
1256 if( ! options::instWhenMode
.wasSetByUser()){
1257 //instantiate only on last call
1258 if( options::fmfInstEngine() ){
1259 Trace("smt") << "setting inst when mode to LAST_CALL" << endl
;
1260 options::instWhenMode
.set( quantifiers::INST_WHEN_LAST_CALL
);
1263 if( d_logic
.hasCardinalityConstraints() ){
1264 //must have finite model finding on
1265 options::finiteModelFind
.set( true );
1267 if( options::recurseCbqi() ){
1268 options::cbqi
.set( true );
1270 if(options::fmfBoundIntLazy
.wasSetByUser() && options::fmfBoundIntLazy()) {
1271 options::fmfBoundInt
.set( true );
1273 if( options::fmfBoundInt() ){
1274 //must have finite model finding on
1275 options::finiteModelFind
.set( true );
1276 if( ! options::mbqiMode
.wasSetByUser() ||
1277 ( options::mbqiMode()!=quantifiers::MBQI_NONE
&&
1278 options::mbqiMode()!=quantifiers::MBQI_FMC
&&
1279 options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL
) ){
1280 //if bounded integers are set, use no MBQI by default
1281 options::mbqiMode
.set( quantifiers::MBQI_NONE
);
1284 if( options::mbqiMode()==quantifiers::MBQI_INTERVAL
){
1285 //must do pre-skolemization
1286 options::preSkolemQuant
.set( true );
1288 if( options::ufssSymBreak() ){
1289 options::sortInference
.set( true );
1291 if( options::qcfMode
.wasSetByUser() || options::qcfTConstraint() ){
1292 options::quantConflictFind
.set( true );
1294 //for induction techniques
1295 if( options::quantInduction() ){
1296 if( !options::dtStcInduction
.wasSetByUser() ){
1297 options::dtStcInduction
.set( true );
1299 if( !options::intWfInduction
.wasSetByUser() ){
1300 options::intWfInduction
.set( true );
1303 if( options::dtStcInduction() ){
1304 //leads to unfairness FIXME
1305 if( !options::dtForceAssignment
.wasSetByUser() ){
1306 options::dtForceAssignment
.set( true );
1309 if( options::intWfInduction() ){
1310 if( !options::purifyTriggers
.wasSetByUser() ){
1311 options::purifyTriggers
.set( true );
1314 if( options::conjectureNoFilter() ){
1315 if( !options::conjectureFilterActiveTerms
.wasSetByUser() ){
1316 options::conjectureFilterActiveTerms
.set( false );
1318 if( !options::conjectureFilterCanonical
.wasSetByUser() ){
1319 options::conjectureFilterCanonical
.set( false );
1321 if( !options::conjectureFilterModel
.wasSetByUser() ){
1322 options::conjectureFilterModel
.set( false );
1326 //until bugs 371,431 are fixed
1327 if( ! options::minisatUseElim
.wasSetByUser()){
1328 if( d_logic
.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){
1329 options::minisatUseElim
.set( false );
1332 else if (options::minisatUseElim()) {
1333 if (options::produceModels()) {
1334 Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << endl
;
1335 setOption("produce-models", SExpr("false"));
1337 if (options::produceAssignments()) {
1338 Notice() << "SmtEngine: turning off produce-assignments to support minisatUseElim" << endl
;
1339 setOption("produce-assignments", SExpr("false"));
1341 if (options::checkModels()) {
1342 Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << endl
;
1343 setOption("check-models", SExpr("false"));
1347 // For now, these array theory optimizations do not support model-building
1348 if (options::produceModels() || options::produceAssignments() || options::checkModels()) {
1349 options::arraysOptimizeLinear
.set(false);
1350 options::arraysLazyRIntro1
.set(false);
1353 // Non-linear arithmetic does not support models
1354 if (d_logic
.isTheoryEnabled(THEORY_ARITH
) &&
1355 !d_logic
.isLinear()) {
1356 if (options::produceModels()) {
1357 Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl
;
1358 setOption("produce-models", SExpr("false"));
1360 if (options::produceAssignments()) {
1361 Warning() << "SmtEngine: turning off produce-assignments because unsupported for nonlinear arith" << endl
;
1362 setOption("produce-assignments", SExpr("false"));
1364 if (options::checkModels()) {
1365 Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl
;
1366 setOption("check-models", SExpr("false"));
1370 if(options::incrementalSolving() && (options::proof() || options::unsatCores())) {
1371 Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof or --produce-unsat-cores, try --tear-down-incremental instead)" << endl
;
1372 setOption("incremental", SExpr("false"));
1376 void SmtEngine::setInfo(const std::string
& key
, const CVC4::SExpr
& value
)
1377 throw(OptionException
, ModalException
) {
1379 SmtScope
smts(this);
1381 Trace("smt") << "SMT setInfo(" << key
<< ", " << value
<< ")" << endl
;
1382 if(Dump
.isOn("benchmark")) {
1383 if(key
== "status") {
1384 string s
= value
.getValue();
1385 BenchmarkStatus status
=
1386 (s
== "sat") ? SMT_SATISFIABLE
:
1387 ((s
== "unsat") ? SMT_UNSATISFIABLE
: SMT_UNKNOWN
);
1388 Dump("benchmark") << SetBenchmarkStatusCommand(status
);
1390 Dump("benchmark") << SetInfoCommand(key
, value
);
1394 // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
1395 if(key
.length() > 5) {
1396 string prefix
= key
.substr(0, 5);
1397 if(prefix
== "cvc4-" || prefix
== "cvc4_") {
1398 string cvc4key
= key
.substr(5);
1399 if(cvc4key
== "logic") {
1400 if(! value
.isAtom()) {
1401 throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
1403 SmtScope
smts(this);
1404 d_logic
= value
.getValue();
1408 throw UnrecognizedOptionException();
1413 // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
1414 if(key
== "source" ||
1415 key
== "category" ||
1416 key
== "difficulty" ||
1420 } else if(key
== "name") {
1421 d_filename
= value
.getValue();
1423 } else if(key
== "smt-lib-version") {
1424 if( (value
.isInteger() && value
.getIntegerValue() == Integer(2)) ||
1425 (value
.isRational() && value
.getRationalValue() == Rational(2)) ||
1426 (value
.getValue() == "2") ) {
1427 // supported SMT-LIB version
1430 Warning() << "Warning: unsupported smt-lib-version: " << value
<< endl
;
1431 throw UnrecognizedOptionException();
1432 } else if(key
== "status") {
1434 if(value
.isAtom()) {
1435 s
= value
.getValue();
1437 if(s
!= "sat" && s
!= "unsat" && s
!= "unknown") {
1438 throw OptionException("argument to (set-info :status ..) must be "
1439 "`sat' or `unsat' or `unknown'");
1441 d_status
= Result(s
, d_filename
);
1444 throw UnrecognizedOptionException();
1447 CVC4::SExpr
SmtEngine::getInfo(const std::string
& key
) const
1448 throw(OptionException
, ModalException
) {
1450 SmtScope
smts(this);
1452 Trace("smt") << "SMT getInfo(" << key
<< ")" << endl
;
1453 if(key
== "all-statistics") {
1454 vector
<SExpr
> stats
;
1455 for(StatisticsRegistry::const_iterator i
= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->begin();
1456 i
!= NodeManager::fromExprManager(d_exprManager
)->getStatisticsRegistry()->end();
1459 v
.push_back((*i
).first
);
1460 v
.push_back((*i
).second
);
1463 for(StatisticsRegistry::const_iterator i
= d_statisticsRegistry
->begin();
1464 i
!= d_statisticsRegistry
->end();
1467 v
.push_back((*i
).first
);
1468 v
.push_back((*i
).second
);
1472 } else if(key
== "error-behavior") {
1473 // immediate-exit | continued-execution
1474 if( options::continuedExecution() || options::interactive() ) {
1475 return SExpr::Keyword("continued-execution");
1477 return SExpr::Keyword("immediate-exit");
1479 } else if(key
== "name") {
1480 return Configuration::getName();
1481 } else if(key
== "version") {
1482 return Configuration::getVersionString();
1483 } else if(key
== "authors") {
1484 return Configuration::about();
1485 } else if(key
== "status") {
1486 // sat | unsat | unknown
1487 switch(d_status
.asSatisfiabilityResult().isSat()) {
1489 return SExpr::Keyword("sat");
1491 return SExpr::Keyword("unsat");
1493 return SExpr::Keyword("unknown");
1495 } else if(key
== "reason-unknown") {
1496 if(!d_status
.isNull() && d_status
.isUnknown()) {
1498 ss
<< d_status
.whyUnknown();
1499 string s
= ss
.str();
1500 transform(s
.begin(), s
.end(), s
.begin(), ::tolower
);
1501 return SExpr::Keyword(s
);
1503 throw ModalException("Can't get-info :reason-unknown when the "
1504 "last result wasn't unknown!");
1506 } else if(key
== "all-options") {
1507 // get the options, like all-statistics
1508 return Options::current().getOptions();
1510 throw UnrecognizedOptionException();
1514 void SmtEngine::defineFunction(Expr func
,
1515 const std::vector
<Expr
>& formals
,
1517 Trace("smt") << "SMT defineFunction(" << func
<< ")" << endl
;
1518 for(std::vector
<Expr
>::const_iterator i
= formals
.begin(); i
!= formals
.end(); ++i
) {
1519 if((*i
).getKind() != kind::BOUND_VARIABLE
) {
1521 ss
<< "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
1522 << "definition of function " << func
<< ", formal\n"
1523 << " " << *i
<< "\n"
1524 << "has kind " << (*i
).getKind();
1525 throw TypeCheckingException(func
, ss
.str());
1530 ss
<< Expr::setlanguage(Expr::setlanguage::getLanguage(Dump
.getStream()))
1532 DefineFunctionCommand
c(ss
.str(), func
, formals
, formula
);
1533 addToModelCommandAndDump(c
, ExprManager::VAR_FLAG_DEFINED
, true, "declarations");
1535 SmtScope
smts(this);
1537 // Substitute out any abstract values in formula
1538 Expr form
= d_private
->substituteAbstractValues(Node::fromExpr(formula
)).toExpr();
1541 Type formulaType
= form
.getType(options::typeChecking());
1543 Type funcType
= func
.getType();
1544 // We distinguish here between definitions of constants and functions,
1545 // because the type checking for them is subtly different. Perhaps we
1546 // should instead have SmtEngine::defineFunction() and
1547 // SmtEngine::defineConstant() for better clarity, although then that
1548 // doesn't match the SMT-LIBv2 standard...
1549 if(formals
.size() > 0) {
1550 Type rangeType
= FunctionType(funcType
).getRangeType();
1551 if(! formulaType
.isComparableTo(rangeType
)) {
1553 ss
<< "Type of defined function does not match its declaration\n"
1554 << "The function : " << func
<< "\n"
1555 << "Declared type : " << rangeType
<< "\n"
1556 << "The body : " << formula
<< "\n"
1557 << "Body type : " << formulaType
;
1558 throw TypeCheckingException(func
, ss
.str());
1561 if(! formulaType
.isComparableTo(funcType
)) {
1563 ss
<< "Declared type of defined constant does not match its definition\n"
1564 << "The constant : " << func
<< "\n"
1565 << "Declared type : " << funcType
<< " " << Type::getTypeNode(funcType
)->getId() << "\n"
1566 << "The definition : " << formula
<< "\n"
1567 << "Definition type: " << formulaType
<< " " << Type::getTypeNode(formulaType
)->getId();
1568 throw TypeCheckingException(func
, ss
.str());
1571 TNode funcNode
= func
.getTNode();
1572 vector
<Node
> formalsNodes
;
1573 for(vector
<Expr
>::const_iterator i
= formals
.begin(),
1574 iend
= formals
.end();
1577 formalsNodes
.push_back((*i
).getNode());
1579 TNode formNode
= form
.getTNode();
1580 DefinedFunction
def(funcNode
, formalsNodes
, formNode
);
1581 // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
1582 // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
1583 // d_haveAdditions = true;
1584 Debug("smt") << "definedFunctions insert " << funcNode
<< " " << formNode
<< endl
;
1585 d_definedFunctions
->insert(funcNode
, def
);
1588 Node
SmtEnginePrivate::expandDefinitions(TNode n
, hash_map
<Node
, Node
, NodeHashFunction
>& cache
, bool expandOnly
)
1589 throw(TypeCheckingException
, LogicException
) {
1591 stack
< triple
<Node
, Node
, bool> > worklist
;
1593 worklist
.push(make_triple(Node(n
), Node(n
), false));
1594 // The worklist is made of triples, each is input / original node then the output / rewritten node
1595 // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
1599 n
= worklist
.top().first
; // n is the input / original
1600 Node node
= worklist
.top().second
; // node is the output / result
1601 bool childrenPushed
= worklist
.top().third
;
1604 // Working downwards
1605 if(!childrenPushed
) {
1606 Kind k
= n
.getKind();
1608 // Apart from apply, we can short circuit leaves
1609 if(k
!= kind::APPLY
&& n
.getNumChildren() == 0) {
1610 SmtEngine::DefinedFunctionMap::const_iterator i
= d_smt
.d_definedFunctions
->find(n
);
1611 if(i
!= d_smt
.d_definedFunctions
->end()) {
1612 // replacement must be closed
1613 if((*i
).second
.getFormals().size() > 0) {
1614 result
.push(d_smt
.d_nodeManager
->mkNode(kind::LAMBDA
, d_smt
.d_nodeManager
->mkNode(kind::BOUND_VAR_LIST
, (*i
).second
.getFormals()), (*i
).second
.getFormula()));
1617 // don't bother putting in the cache
1618 result
.push((*i
).second
.getFormula());
1621 // don't bother putting in the cache
1626 // maybe it's in the cache
1627 hash_map
<Node
, Node
, NodeHashFunction
>::iterator cacheHit
= cache
.find(n
);
1628 if(cacheHit
!= cache
.end()) {
1629 TNode ret
= (*cacheHit
).second
;
1630 result
.push(ret
.isNull() ? n
: ret
);
1634 // otherwise expand it
1635 if (k
== kind::APPLY
) {
1636 // application of a user-defined symbol
1637 TNode func
= n
.getOperator();
1638 SmtEngine::DefinedFunctionMap::const_iterator i
=
1639 d_smt
.d_definedFunctions
->find(func
);
1640 DefinedFunction def
= (*i
).second
;
1641 vector
<Node
> formals
= def
.getFormals();
1643 if(Debug
.isOn("expand")) {
1644 Debug("expand") << "found: " << n
<< endl
;
1645 Debug("expand") << " func: " << func
<< endl
;
1646 string name
= func
.getAttribute(expr::VarNameAttr());
1647 Debug("expand") << " : \"" << name
<< "\"" << endl
;
1649 if(i
== d_smt
.d_definedFunctions
->end()) {
1650 throw TypeCheckingException(n
.toExpr(), string("Undefined function: `") + func
.toString() + "'");
1652 if(Debug
.isOn("expand")) {
1653 Debug("expand") << " defn: " << def
.getFunction() << endl
1655 if(formals
.size() > 0) {
1656 copy( formals
.begin(), formals
.end() - 1,
1657 ostream_iterator
<Node
>(Debug("expand"), ", ") );
1658 Debug("expand") << formals
.back();
1660 Debug("expand") << "]" << endl
1661 << " " << def
.getFunction().getType() << endl
1662 << " " << def
.getFormula() << endl
;
1665 TNode fm
= def
.getFormula();
1666 Node instance
= fm
.substitute(formals
.begin(), formals
.end(),
1667 n
.begin(), n
.end());
1668 Debug("expand") << "made : " << instance
<< endl
;
1670 Node expanded
= expandDefinitions(instance
, cache
, expandOnly
);
1671 cache
[n
] = (n
== expanded
? Node::null() : expanded
);
1672 result
.push(expanded
);
1675 } else if(! expandOnly
) {
1676 // do not do any theory stuff if expandOnly is true
1678 theory::Theory
* t
= d_smt
.d_theoryEngine
->theoryOf(node
);
1681 LogicRequest
req(d_smt
);
1682 node
= t
->expandDefinition(req
, n
);
1685 // there should be children here, otherwise we short-circuited a result-push/continue, above
1686 if (node
.getNumChildren() == 0) {
1687 Debug("expand") << "Unexpectedly no children..." << node
<< endl
;
1689 // This invariant holds at the moment but it is concievable that a new theory
1690 // might introduce a kind which can have children before definition expansion but doesn't
1691 // afterwards. If this happens, remove this assertion.
1692 Assert(node
.getNumChildren() > 0);
1694 // the partial functions can fall through, in which case we still
1695 // consider their children
1696 worklist
.push(make_triple(Node(n
), node
, true)); // Original and rewritten result
1698 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
1699 worklist
.push(make_triple(node
[i
], node
[i
], false)); // Rewrite the children of the result only
1704 // Reconstruct the node from it's (now rewritten) children on the stack
1706 Debug("expand") << "cons : " << node
<< endl
;
1707 //cout << "cons : " << node << endl;
1708 NodeBuilder
<> nb(node
.getKind());
1709 if(node
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
1710 Debug("expand") << "op : " << node
.getOperator() << endl
;
1711 //cout << "op : " << node.getOperator() << endl;
1712 nb
<< node
.getOperator();
1714 for(size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
1715 Assert(!result
.empty());
1716 Node expanded
= result
.top();
1718 //cout << "exchld : " << expanded << endl;
1719 Debug("expand") << "exchld : " << expanded
<< endl
;
1723 cache
[n
] = n
== node
? Node::null() : node
; // Only cache once all subterms are expanded
1726 } while(!worklist
.empty());
1728 AlwaysAssert(result
.size() == 1);
1730 return result
.top();
1733 void SmtEnginePrivate::removeITEs() {
1734 d_smt
.finalOptionsAreSet();
1736 Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl
;
1738 // Remove all of the ITE occurrences and normalize
1739 d_iteRemover
.run(d_assertions
.ref(), d_iteSkolemMap
, true);
1740 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
1741 d_assertions
.replace(i
, Rewriter::rewrite(d_assertions
[i
]));
1745 void SmtEnginePrivate::staticLearning() {
1746 d_smt
.finalOptionsAreSet();
1748 TimerStat::CodeTimer
staticLearningTimer(d_smt
.d_stats
->d_staticLearningTime
);
1750 Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl
;
1752 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
1754 NodeBuilder
<> learned(kind::AND
);
1755 learned
<< d_assertions
[i
];
1756 d_smt
.d_theoryEngine
->ppStaticLearn(d_assertions
[i
], learned
);
1757 if(learned
.getNumChildren() == 1) {
1760 d_assertions
.replace(i
, learned
);
1765 // do dumping (before/after any preprocessing pass)
1766 static void dumpAssertions(const char* key
, const AssertionPipeline
& assertionList
) {
1767 if( Dump
.isOn("assertions") &&
1768 Dump
.isOn(string("assertions:") + key
) ) {
1769 // Push the simplified assertions to the dump output stream
1770 for(unsigned i
= 0; i
< assertionList
.size(); ++ i
) {
1771 TNode n
= assertionList
[i
];
1772 Dump("assertions") << AssertCommand(Expr(n
.toExpr()));
1777 // returns false if it learns a conflict
1778 bool SmtEnginePrivate::nonClausalSimplify() {
1779 d_smt
.finalOptionsAreSet();
1781 if(options::unsatCores()) {
1785 TimerStat::CodeTimer
nonclausalTimer(d_smt
.d_stats
->d_nonclausalSimplificationTime
);
1787 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl
;
1789 if(d_propagatorNeedsFinish
) {
1790 d_propagator
.finish();
1791 d_propagatorNeedsFinish
= false;
1793 d_propagator
.initialize();
1795 // Assert all the assertions to the propagator
1796 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1797 << "asserting to propagator" << endl
;
1798 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
1799 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
1800 // Don't reprocess substitutions
1801 if (d_substitutionsIndex
> 0 && i
== d_substitutionsIndex
) {
1804 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions
[i
] << endl
;
1805 Debug("cores") << "d_propagator assertTrue: " << d_assertions
[i
] << std::endl
;
1806 d_propagator
.assertTrue(d_assertions
[i
]);
1809 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1810 << "propagating" << endl
;
1811 if (d_propagator
.propagate()) {
1812 // If in conflict, just return false
1813 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1814 << "conflict in non-clausal propagation" << endl
;
1815 Node falseNode
= NodeManager::currentNM()->mkConst
<bool>(false);
1816 Assert(!options::unsatCores());
1817 d_assertions
.clear();
1818 d_assertions
.push_back(falseNode
);
1819 d_propagatorNeedsFinish
= true;
1823 // No conflict, go through the literals and solve them
1824 SubstitutionMap
constantPropagations(d_smt
.d_context
);
1825 SubstitutionMap
newSubstitutions(d_smt
.d_context
);
1826 SubstitutionMap::iterator pos
;
1828 for(unsigned i
= 0, i_end
= d_nonClausalLearnedLiterals
.size(); i
< i_end
; ++ i
) {
1829 // Simplify the literal we learned wrt previous substitutions
1830 Node learnedLiteral
= d_nonClausalLearnedLiterals
[i
];
1831 Assert(Rewriter::rewrite(learnedLiteral
) == learnedLiteral
);
1832 Assert(d_topLevelSubstitutions
.apply(learnedLiteral
) == learnedLiteral
);
1833 Node learnedLiteralNew
= newSubstitutions
.apply(learnedLiteral
);
1834 if (learnedLiteral
!= learnedLiteralNew
) {
1835 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
1838 learnedLiteralNew
= constantPropagations
.apply(learnedLiteral
);
1839 if (learnedLiteralNew
== learnedLiteral
) {
1842 ++d_smt
.d_stats
->d_numConstantProps
;
1843 learnedLiteral
= Rewriter::rewrite(learnedLiteralNew
);
1845 // It might just simplify to a constant
1846 if (learnedLiteral
.isConst()) {
1847 if (learnedLiteral
.getConst
<bool>()) {
1848 // If the learned literal simplifies to true, it's redundant
1851 // If the learned literal simplifies to false, we're in conflict
1852 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1854 << d_nonClausalLearnedLiterals
[i
] << endl
;
1855 Assert(!options::unsatCores());
1856 d_assertions
.clear();
1857 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(false));
1858 d_propagatorNeedsFinish
= true;
1863 // Solve it with the corresponding theory, possibly adding new
1864 // substitutions to newSubstitutions
1865 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1866 << "solving " << learnedLiteral
<< endl
;
1868 Theory::PPAssertStatus solveStatus
=
1869 d_smt
.d_theoryEngine
->solve(learnedLiteral
, newSubstitutions
);
1871 switch (solveStatus
) {
1872 case Theory::PP_ASSERT_STATUS_SOLVED
: {
1873 // The literal should rewrite to true
1874 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1875 << "solved " << learnedLiteral
<< endl
;
1876 Assert(Rewriter::rewrite(newSubstitutions
.apply(learnedLiteral
)).isConst());
1877 // vector<pair<Node, Node> > equations;
1878 // constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true);
1879 // if (equations.empty()) {
1882 // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
1883 // else fall through
1886 case Theory::PP_ASSERT_STATUS_CONFLICT
:
1887 // If in conflict, we return false
1888 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1889 << "conflict while solving "
1890 << learnedLiteral
<< endl
;
1891 Assert(!options::unsatCores());
1892 d_assertions
.clear();
1893 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(false));
1894 d_propagatorNeedsFinish
= true;
1897 if (d_doConstantProp
&& learnedLiteral
.getKind() == kind::EQUAL
&& (learnedLiteral
[0].isConst() || learnedLiteral
[1].isConst())) {
1898 // constant propagation
1901 if (learnedLiteral
[0].isConst()) {
1902 t
= learnedLiteral
[1];
1903 c
= learnedLiteral
[0];
1906 t
= learnedLiteral
[0];
1907 c
= learnedLiteral
[1];
1909 Assert(!t
.isConst());
1910 Assert(constantPropagations
.apply(t
) == t
);
1911 Assert(d_topLevelSubstitutions
.apply(t
) == t
);
1912 Assert(newSubstitutions
.apply(t
) == t
);
1913 constantPropagations
.addSubstitution(t
, c
);
1914 // vector<pair<Node,Node> > equations;
1915 // constantPropagations.simplifyLHS(t, c, equations, true);
1916 // if (!equations.empty()) {
1917 // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
1918 // d_assertions.clear();
1919 // d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
1922 // d_topLevelSubstitutions.simplifyRHS(constantPropagations);
1926 d_nonClausalLearnedLiterals
[j
++] = d_nonClausalLearnedLiterals
[i
];
1931 #ifdef CVC4_ASSERTIONS
1932 // Check data structure invariants:
1933 // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations
1934 // 2. each lhs of constantPropagations rewrites to itself
1935 // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a
1936 // constant propagation too
1937 // 4. each lhs of constantPropagations is different from each rhs
1938 for (pos
= newSubstitutions
.begin(); pos
!= newSubstitutions
.end(); ++pos
) {
1939 Assert((*pos
).first
.isVar());
1940 Assert(d_topLevelSubstitutions
.apply((*pos
).first
) == (*pos
).first
);
1941 Assert(d_topLevelSubstitutions
.apply((*pos
).second
) == (*pos
).second
);
1942 Assert(newSubstitutions
.apply(newSubstitutions
.apply((*pos
).second
)) == newSubstitutions
.apply((*pos
).second
));
1944 for (pos
= constantPropagations
.begin(); pos
!= constantPropagations
.end(); ++pos
) {
1945 Assert((*pos
).second
.isConst());
1946 Assert(Rewriter::rewrite((*pos
).first
) == (*pos
).first
);
1947 // Node newLeft = d_topLevelSubstitutions.apply((*pos).first);
1948 // if (newLeft != (*pos).first) {
1949 // newLeft = Rewriter::rewrite(newLeft);
1950 // Assert(newLeft == (*pos).second ||
1951 // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
1953 // newLeft = constantPropagations.apply((*pos).first);
1954 // if (newLeft != (*pos).first) {
1955 // newLeft = Rewriter::rewrite(newLeft);
1956 // Assert(newLeft == (*pos).second ||
1957 // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
1959 Assert(constantPropagations
.apply((*pos
).second
) == (*pos
).second
);
1961 #endif /* CVC4_ASSERTIONS */
1963 // Resize the learnt
1964 d_nonClausalLearnedLiterals
.resize(j
);
1966 hash_set
<TNode
, TNodeHashFunction
> s
;
1967 Trace("debugging") << "NonClausal simplify pre-preprocess\n";
1968 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
1969 Node assertion
= d_assertions
[i
];
1970 Node assertionNew
= newSubstitutions
.apply(assertion
);
1971 Trace("debugging") << "assertion = " << assertion
<< endl
;
1972 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
1973 if (assertion
!= assertionNew
) {
1974 assertion
= Rewriter::rewrite(assertionNew
);
1975 Trace("debugging") << "rewrite(assertion) = " << assertion
<< endl
;
1977 Assert(Rewriter::rewrite(assertion
) == assertion
);
1979 assertionNew
= constantPropagations
.apply(assertion
);
1980 if (assertionNew
== assertion
) {
1983 ++d_smt
.d_stats
->d_numConstantProps
;
1984 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
1985 assertion
= Rewriter::rewrite(assertionNew
);
1986 Trace("debugging") << "assertionNew = " << assertionNew
<< endl
;
1988 Trace("debugging") << "\n";
1989 s
.insert(assertion
);
1990 d_assertions
.replace(i
, assertion
);
1991 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
1992 << "non-clausal preprocessed: "
1993 << assertion
<< endl
;
1996 // If in incremental mode, add substitutions to the list of assertions
1997 if (d_substitutionsIndex
> 0) {
1998 NodeBuilder
<> substitutionsBuilder(kind::AND
);
1999 substitutionsBuilder
<< d_assertions
[d_substitutionsIndex
];
2000 pos
= newSubstitutions
.begin();
2001 for (; pos
!= newSubstitutions
.end(); ++pos
) {
2002 // Add back this substitution as an assertion
2003 TNode lhs
= (*pos
).first
, rhs
= newSubstitutions
.apply((*pos
).second
);
2004 Node n
= NodeManager::currentNM()->mkNode(lhs
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, lhs
, rhs
);
2005 substitutionsBuilder
<< n
;
2006 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n
<< endl
;
2008 if (substitutionsBuilder
.getNumChildren() > 1) {
2009 d_assertions
.replace(d_substitutionsIndex
,
2010 Rewriter::rewrite(Node(substitutionsBuilder
)));
2013 // If not in incremental mode, must add substitutions to model
2014 TheoryModel
* m
= d_smt
.d_theoryEngine
->getModel();
2016 for(pos
= newSubstitutions
.begin(); pos
!= newSubstitutions
.end(); ++pos
) {
2017 Node n
= (*pos
).first
;
2018 Node v
= newSubstitutions
.apply((*pos
).second
);
2019 Trace("model") << "Add substitution : " << n
<< " " << v
<< endl
;
2020 m
->addSubstitution( n
, v
);
2025 NodeBuilder
<> learnedBuilder(kind::AND
);
2026 Assert(d_realAssertionsEnd
<= d_assertions
.size());
2027 learnedBuilder
<< d_assertions
[d_realAssertionsEnd
- 1];
2029 for (unsigned i
= 0; i
< d_nonClausalLearnedLiterals
.size(); ++ i
) {
2030 Node learned
= d_nonClausalLearnedLiterals
[i
];
2031 Assert(d_topLevelSubstitutions
.apply(learned
) == learned
);
2032 Node learnedNew
= newSubstitutions
.apply(learned
);
2033 if (learned
!= learnedNew
) {
2034 learned
= Rewriter::rewrite(learnedNew
);
2036 Assert(Rewriter::rewrite(learned
) == learned
);
2038 learnedNew
= constantPropagations
.apply(learned
);
2039 if (learnedNew
== learned
) {
2042 ++d_smt
.d_stats
->d_numConstantProps
;
2043 learned
= Rewriter::rewrite(learnedNew
);
2045 if (s
.find(learned
) != s
.end()) {
2049 learnedBuilder
<< learned
;
2050 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2051 << "non-clausal learned : "
2054 d_nonClausalLearnedLiterals
.clear();
2056 for (pos
= constantPropagations
.begin(); pos
!= constantPropagations
.end(); ++pos
) {
2057 Node cProp
= (*pos
).first
.eqNode((*pos
).second
);
2058 Assert(d_topLevelSubstitutions
.apply(cProp
) == cProp
);
2059 Node cPropNew
= newSubstitutions
.apply(cProp
);
2060 if (cProp
!= cPropNew
) {
2061 cProp
= Rewriter::rewrite(cPropNew
);
2062 Assert(Rewriter::rewrite(cProp
) == cProp
);
2064 if (s
.find(cProp
) != s
.end()) {
2068 learnedBuilder
<< cProp
;
2069 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2070 << "non-clausal constant propagation : "
2074 // Add new substitutions to topLevelSubstitutions
2075 // Note that we don't have to keep rhs's in full solved form
2076 // because SubstitutionMap::apply does a fixed-point iteration when substituting
2077 d_topLevelSubstitutions
.addSubstitutions(newSubstitutions
);
2079 if(learnedBuilder
.getNumChildren() > 1) {
2080 d_assertions
.replace(d_realAssertionsEnd
- 1,
2081 Rewriter::rewrite(Node(learnedBuilder
)));
2084 d_propagatorNeedsFinish
= true;
2088 void SmtEnginePrivate::bvAbstraction() {
2089 Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl
;
2090 std::vector
<Node
> new_assertions
;
2091 bool changed
= d_smt
.d_theoryEngine
->ppBvAbstraction(d_assertions
.ref(), new_assertions
);
2092 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2093 d_assertions
.replace(i
, Rewriter::rewrite(new_assertions
[i
]));
2095 // if we are using the lazy solver and the abstraction
2096 // applies, then UF symbols were introduced
2097 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
&&
2099 LogicRequest
req(d_smt
);
2100 req
.widenLogic(THEORY_UF
);
2105 void SmtEnginePrivate::bvToBool() {
2106 Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl
;
2107 std::vector
<Node
> new_assertions
;
2108 d_smt
.d_theoryEngine
->ppBvToBool(d_assertions
.ref(), new_assertions
);
2109 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2110 d_assertions
.replace(i
, Rewriter::rewrite(new_assertions
[i
]));
2114 bool SmtEnginePrivate::simpITE() {
2115 TimerStat::CodeTimer
simpITETimer(d_smt
.d_stats
->d_simpITETime
);
2117 Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl
;
2119 unsigned numAssertionOnEntry
= d_assertions
.size();
2120 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
2121 Node result
= d_smt
.d_theoryEngine
->ppSimpITE(d_assertions
[i
]);
2122 d_assertions
.replace(i
, result
);
2123 if(result
.isConst() && !result
.getConst
<bool>()){
2127 bool result
= d_smt
.d_theoryEngine
->donePPSimpITE(d_assertions
.ref());
2128 if(numAssertionOnEntry
< d_assertions
.size()){
2129 compressBeforeRealAssertions(numAssertionOnEntry
);
2134 void SmtEnginePrivate::compressBeforeRealAssertions(size_t before
){
2135 size_t curr
= d_assertions
.size();
2136 if(before
>= curr
||
2137 d_realAssertionsEnd
<= 0 ||
2138 d_realAssertionsEnd
>= curr
){
2143 // original: [0 ... d_realAssertionsEnd)
2145 // ites skolems [d_realAssertionsEnd, before)
2147 // added [before, curr)
2149 Assert(0 < d_realAssertionsEnd
);
2150 Assert(d_realAssertionsEnd
<= before
);
2151 Assert(before
< curr
);
2153 std::vector
<Node
> intoConjunction
;
2154 for(size_t i
= before
; i
<curr
; ++i
){
2155 intoConjunction
.push_back(d_assertions
[i
]);
2157 d_assertions
.resize(before
);
2158 size_t lastBeforeItes
= d_realAssertionsEnd
- 1;
2159 intoConjunction
.push_back(d_assertions
[lastBeforeItes
]);
2160 Node newLast
= util::NaryBuilder::mkAssoc(kind::AND
, intoConjunction
);
2161 d_assertions
.replace(lastBeforeItes
, newLast
);
2162 Assert(d_assertions
.size() == before
);
2165 void SmtEnginePrivate::unconstrainedSimp() {
2166 TimerStat::CodeTimer
unconstrainedSimpTimer(d_smt
.d_stats
->d_unconstrainedSimpTime
);
2167 Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl
;
2168 d_smt
.d_theoryEngine
->ppUnconstrainedSimp(d_assertions
.ref());
2172 void SmtEnginePrivate::constrainSubtypes(TNode top
, AssertionPipeline
& assertions
)
2175 Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top
<< endl
;
2178 stack
<TNode
> worklist
;
2183 TNode n
= worklist
.top();
2186 TypeNode t
= n
.getType();
2187 if(t
.isPredicateSubtype()) {
2188 WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl
;
2189 Node pred
= t
.getSubtypePredicate();
2191 // pred can be a LAMBDA, a function constant, or a datatype tester
2192 Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred
.getType() << endl
;
2193 if(d_smt
.d_definedFunctions
->find(pred
) != d_smt
.d_definedFunctions
->end()) {
2195 } else if(pred
.getType().isTester()) {
2196 k
= kind::APPLY_TESTER
;
2200 Node app
= NodeManager::currentNM()->mkNode(k
, pred
, n
);
2201 Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k
<< ") " << app
<< endl
;
2202 assertions
.push_back(app
);
2203 } else if(t
.isSubrange()) {
2204 SubrangeBounds bounds
= t
.getSubrangeBounds();
2205 Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds
<< endl
;
2206 if(bounds
.lower
.hasBound()) {
2207 Node c
= NodeManager::currentNM()->mkConst(Rational(bounds
.lower
.getBound()));
2208 Node lb
= NodeManager::currentNM()->mkNode(kind::LEQ
, c
, n
);
2209 Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb
<< endl
;
2210 assertions
.push_back(lb
);
2212 if(bounds
.upper
.hasBound()) {
2213 Node c
= NodeManager::currentNM()->mkConst(Rational(bounds
.upper
.getBound()));
2214 Node ub
= NodeManager::currentNM()->mkNode(kind::LEQ
, n
, c
);
2215 Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub
<< endl
;
2216 assertions
.push_back(ub
);
2220 for(TNode::iterator i
= n
.begin(); i
!= n
.end(); ++i
) {
2221 if(done
.find(*i
) == done
.end()) {
2226 } while(! worklist
.empty());
2229 void SmtEnginePrivate::traceBackToAssertions(const std::vector
<Node
>& nodes
, std::vector
<TNode
>& assertions
) {
2230 const booleans::CircuitPropagator::BackEdgesMap
& backEdges
= d_propagator
.getBackEdges();
2231 for(vector
<Node
>::const_iterator i
= nodes
.begin(); i
!= nodes
.end(); ++i
) {
2232 booleans::CircuitPropagator::BackEdgesMap::const_iterator j
= backEdges
.find(*i
);
2233 // term must appear in map, otherwise how did we get here?!
2234 Assert(j
!= backEdges
.end());
2235 // if term maps to empty, that means it's a top-level assertion
2236 if(!(*j
).second
.empty()) {
2237 traceBackToAssertions((*j
).second
, assertions
);
2239 assertions
.push_back(*i
);
2244 size_t SmtEnginePrivate::removeFromConjunction(Node
& n
, const std::hash_set
<unsigned long>& toRemove
) {
2245 Assert(n
.getKind() == kind::AND
);
2246 size_t removals
= 0;
2247 for(Node::iterator j
= n
.begin(); j
!= n
.end(); ++j
) {
2248 size_t subremovals
= 0;
2250 if(toRemove
.find(sub
.getId()) != toRemove
.end() ||
2251 (sub
.getKind() == kind::AND
&& (subremovals
= removeFromConjunction(sub
, toRemove
)) > 0)) {
2252 NodeBuilder
<> b(kind::AND
);
2253 b
.append(n
.begin(), j
);
2254 if(subremovals
> 0) {
2255 removals
+= subremovals
;
2260 for(++j
; j
!= n
.end(); ++j
) {
2261 if(toRemove
.find((*j
).getId()) != toRemove
.end()) {
2263 } else if((*j
).getKind() == kind::AND
) {
2265 if((subremovals
= removeFromConjunction(sub
, toRemove
)) > 0) {
2266 removals
+= subremovals
;
2275 if(b
.getNumChildren() == 0) {
2278 } else if(b
.getNumChildren() == 1) {
2284 n
= Rewriter::rewrite(n
);
2289 Assert(removals
== 0);
2293 void SmtEnginePrivate::doMiplibTrick() {
2294 Assert(d_realAssertionsEnd
== d_assertions
.size());
2295 Assert(!options::incrementalSolving());
2297 const booleans::CircuitPropagator::BackEdgesMap
& backEdges
= d_propagator
.getBackEdges();
2298 hash_set
<unsigned long> removeAssertions
;
2300 NodeManager
* nm
= NodeManager::currentNM();
2301 Node zero
= nm
->mkConst(Rational(0)), one
= nm
->mkConst(Rational(1));
2303 hash_map
<TNode
, Node
, TNodeHashFunction
> intVars
;
2304 for(vector
<Node
>::const_iterator i
= d_boolVars
.begin(); i
!= d_boolVars
.end(); ++i
) {
2305 if(d_propagator
.isAssigned(*i
)) {
2306 Debug("miplib") << "ineligible: " << *i
<< " because assigned " << d_propagator
.getAssignment(*i
) << endl
;
2310 vector
<TNode
> assertions
;
2311 booleans::CircuitPropagator::BackEdgesMap::const_iterator j
= backEdges
.find(*i
);
2312 // if not in back edges map, the bool var is unconstrained, showing up in no assertions.
2313 // if maps to an empty vector, that means the bool var was asserted itself.
2314 if(j
!= backEdges
.end()) {
2315 if(!(*j
).second
.empty()) {
2316 traceBackToAssertions((*j
).second
, assertions
);
2318 assertions
.push_back(*i
);
2321 Debug("miplib") << "for " << *i
<< endl
;
2322 bool eligible
= true;
2323 map
<pair
<Node
, Node
>, uint64_t> marks
;
2324 map
<pair
<Node
, Node
>, vector
<Rational
> > coef
;
2325 map
<pair
<Node
, Node
>, vector
<Rational
> > checks
;
2326 map
<pair
<Node
, Node
>, vector
<TNode
> > asserts
;
2327 for(vector
<TNode
>::const_iterator j
= assertions
.begin(); j
!= assertions
.end(); ++j
) {
2328 Debug("miplib") << " found: " << *j
<< endl
;
2329 if((*j
).getKind() != kind::IMPLIES
) {
2331 Debug("miplib") << " -- INELIGIBLE -- (not =>)" << endl
;
2334 Node conj
= BooleanSimplification::simplify((*j
)[0]);
2335 if(conj
.getKind() == kind::AND
&& conj
.getNumChildren() > 6) {
2337 Debug("miplib") << " -- INELIGIBLE -- (N-ary /\\ too big)" << endl
;
2340 if(conj
.getKind() != kind::AND
&& !conj
.isVar() && !(conj
.getKind() == kind::NOT
&& conj
[0].isVar())) {
2342 Debug("miplib") << " -- INELIGIBLE -- (not /\\ or literal)" << endl
;
2345 if((*j
)[1].getKind() != kind::EQUAL
||
2346 !( ( (*j
)[1][0].isVar() &&
2347 (*j
)[1][1].getKind() == kind::CONST_RATIONAL
) ||
2348 ( (*j
)[1][0].getKind() == kind::CONST_RATIONAL
&&
2349 (*j
)[1][1].isVar() ) )) {
2351 Debug("miplib") << " -- INELIGIBLE -- (=> (and X X) X)" << endl
;
2354 if(conj
.getKind() == kind::AND
) {
2356 bool found_x
= false;
2357 map
<TNode
, bool> neg
;
2358 for(Node::iterator ii
= conj
.begin(); ii
!= conj
.end(); ++ii
) {
2360 posv
.push_back(*ii
);
2362 found_x
= found_x
|| *i
== *ii
;
2363 } else if((*ii
).getKind() == kind::NOT
&& (*ii
)[0].isVar()) {
2364 posv
.push_back((*ii
)[0]);
2365 neg
[(*ii
)[0]] = true;
2366 found_x
= found_x
|| *i
== (*ii
)[0];
2369 Debug("miplib") << " -- INELIGIBLE -- (non-var: " << *ii
<< ")" << endl
;
2372 if(d_propagator
.isAssigned(posv
.back())) {
2374 Debug("miplib") << " -- INELIGIBLE -- (" << posv
.back() << " asserted)" << endl
;
2383 Debug("miplib") << " --INELIGIBLE -- (couldn't find " << *i
<< " in conjunction)" << endl
;
2386 sort(posv
.begin(), posv
.end());
2387 const Node pos
= NodeManager::currentNM()->mkNode(kind::AND
, posv
);
2388 const TNode var
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][1] : (*j
)[1][0];
2389 const pair
<Node
, Node
> pos_var(pos
, var
);
2390 const Rational
& constant
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][0].getConst
<Rational
>() : (*j
)[1][1].getConst
<Rational
>();
2392 unsigned countneg
= 0, thepos
= 0;
2393 for(unsigned ii
= 0; ii
< pos
.getNumChildren(); ++ii
) {
2398 mark
|= (0x1 << ii
);
2401 if((marks
[pos_var
] & (1lu << mark
)) != 0) {
2403 Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl
;
2406 Debug("miplib") << "mark is " << mark
<< " -- " << (1lu << mark
) << endl
;
2407 marks
[pos_var
] |= (1lu << mark
);
2408 Debug("miplib") << "marks[" << pos
<< "," << var
<< "] now " << marks
[pos_var
] << endl
;
2409 if(countneg
== pos
.getNumChildren()) {
2412 Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl
;
2415 } else if(countneg
== pos
.getNumChildren() - 1) {
2416 Assert(coef
[pos_var
].size() <= 6 && thepos
< 6);
2417 if(coef
[pos_var
].size() <= thepos
) {
2418 coef
[pos_var
].resize(thepos
+ 1);
2420 coef
[pos_var
][thepos
] = constant
;
2422 if(checks
[pos_var
].size() <= mark
) {
2423 checks
[pos_var
].resize(mark
+ 1);
2425 checks
[pos_var
][mark
] = constant
;
2427 asserts
[pos_var
].push_back(*j
);
2430 if(x
!= *i
&& x
!= (*i
).notNode()) {
2432 Debug("miplib") << " -- INELIGIBLE -- (x not present where I expect it)" << endl
;
2435 const bool xneg
= (x
.getKind() == kind::NOT
);
2436 x
= xneg
? x
[0] : x
;
2437 Debug("miplib") << " x:" << x
<< " " << xneg
<< endl
;
2438 const TNode var
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][1] : (*j
)[1][0];
2439 const pair
<Node
, Node
> x_var(x
, var
);
2440 const Rational
& constant
= ((*j
)[1][0].getKind() == kind::CONST_RATIONAL
) ? (*j
)[1][0].getConst
<Rational
>() : (*j
)[1][1].getConst
<Rational
>();
2441 unsigned mark
= (xneg
? 0 : 1);
2442 if((marks
[x_var
] & (1u << mark
)) != 0) {
2444 Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl
;
2447 marks
[x_var
] |= (1u << mark
);
2451 Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl
;
2455 Assert(coef
[x_var
].size() <= 6);
2456 coef
[x_var
].resize(6);
2457 coef
[x_var
][0] = constant
;
2459 asserts
[x_var
].push_back(*j
);
2463 for(map
<pair
<Node
, Node
>, uint64_t>::const_iterator j
= marks
.begin(); j
!= marks
.end(); ++j
) {
2464 const TNode pos
= (*j
).first
.first
;
2465 const TNode var
= (*j
).first
.second
;
2466 const pair
<Node
, Node
>& pos_var
= (*j
).first
;
2467 const uint64_t mark
= (*j
).second
;
2468 const unsigned numVars
= pos
.getKind() == kind::AND
? pos
.getNumChildren() : 1;
2469 uint64_t expected
= (uint64_t(1) << (1 << numVars
)) - 1;
2470 expected
= (expected
== 0) ? -1 : expected
; // fix for overflow
2471 Debug("miplib") << "[" << pos
<< "] => " << hex
<< mark
<< " expect " << expected
<< dec
<< endl
;
2472 Assert(pos
.getKind() == kind::AND
|| pos
.isVar());
2473 if(mark
!= expected
) {
2474 Debug("miplib") << " -- INELIGIBLE " << pos
<< " -- (insufficiently marked, got " << mark
<< " for " << numVars
<< " vars, expected " << expected
<< endl
;
2476 if(mark
!= 3) { // exclude single-var case; nothing to check there
2477 uint64_t sz
= (uint64_t(1) << checks
[pos_var
].size()) - 1;
2478 sz
= (sz
== 0) ? -1 : sz
; // fix for overflow
2479 Assert(sz
== mark
, "expected size %u == mark %u", sz
, mark
);
2480 for(size_t k
= 0; k
< checks
[pos_var
].size(); ++k
) {
2481 if((k
& (k
- 1)) != 0) {
2483 Debug("miplib") << k
<< " => " << checks
[pos_var
][k
] << endl
;
2484 for(size_t v
= 1, kk
= k
; kk
!= 0; ++v
, kk
>>= 1) {
2485 if((kk
& 0x1) == 1) {
2486 Assert(pos
.getKind() == kind::AND
);
2487 Debug("miplib") << "var " << v
<< " : " << pos
[v
- 1] << " coef:" << coef
[pos_var
][v
- 1] << endl
;
2488 sum
+= coef
[pos_var
][v
- 1];
2491 Debug("miplib") << "checkSum is " << sum
<< " input says " << checks
[pos_var
][k
] << endl
;
2492 if(sum
!= checks
[pos_var
][k
]) {
2494 Debug("miplib") << " -- INELIGIBLE " << pos
<< " -- (nonlinear combination)" << endl
;
2498 Assert(checks
[pos_var
][k
] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos
.toString().c_str(), var
.toString().c_str(), k
, checks
[pos_var
][k
].toString().c_str()); // we never set for single-positive-var
2503 eligible
= true; // next is still eligible
2507 Debug("miplib") << " -- ELIGIBLE " << *i
<< " , " << pos
<< " --" << endl
;
2508 vector
<Node
> newVars
;
2509 expr::NodeSelfIterator ii
, iiend
;
2510 if(pos
.getKind() == kind::AND
) {
2514 ii
= expr::NodeSelfIterator::self(pos
);
2515 iiend
= expr::NodeSelfIterator::selfEnd(pos
);
2517 for(; ii
!= iiend
; ++ii
) {
2518 Node
& varRef
= intVars
[*ii
];
2519 if(varRef
.isNull()) {
2521 ss
<< "mipvar_" << *ii
;
2522 Node newVar
= nm
->mkSkolem(ss
.str(), nm
->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME
);
2523 Node geq
= Rewriter::rewrite(nm
->mkNode(kind::GEQ
, newVar
, zero
));
2524 Node leq
= Rewriter::rewrite(nm
->mkNode(kind::LEQ
, newVar
, one
));
2525 d_assertions
.push_back(Rewriter::rewrite(geq
.andNode(leq
)));
2526 SubstitutionMap
nullMap(&d_fakeContext
);
2527 Theory::PPAssertStatus status CVC4_UNUSED
; // just for assertions
2528 status
= d_smt
.d_theoryEngine
->solve(geq
, nullMap
);
2529 Assert(status
== Theory::PP_ASSERT_STATUS_UNSOLVED
,
2530 "unexpected solution from arith's ppAssert()");
2531 Assert(nullMap
.empty(),
2532 "unexpected substitution from arith's ppAssert()");
2533 status
= d_smt
.d_theoryEngine
->solve(leq
, nullMap
);
2534 Assert(status
== Theory::PP_ASSERT_STATUS_UNSOLVED
,
2535 "unexpected solution from arith's ppAssert()");
2536 Assert(nullMap
.empty(),
2537 "unexpected substitution from arith's ppAssert()");
2538 d_smt
.d_theoryEngine
->getModel()->addSubstitution(*ii
, newVar
.eqNode(one
));
2539 newVars
.push_back(newVar
);
2542 newVars
.push_back(varRef
);
2544 if(!d_smt
.d_logic
.areIntegersUsed()) {
2545 d_smt
.d_logic
= d_smt
.d_logic
.getUnlockedCopy();
2546 d_smt
.d_logic
.enableIntegers();
2547 d_smt
.d_logic
.lock();
2551 if(pos
.getKind() == kind::AND
) {
2552 NodeBuilder
<> sumb(kind::PLUS
);
2553 for(size_t ii
= 0; ii
< pos
.getNumChildren(); ++ii
) {
2554 sumb
<< nm
->mkNode(kind::MULT
, nm
->mkConst(coef
[pos_var
][ii
]), newVars
[ii
]);
2558 sum
= nm
->mkNode(kind::MULT
, nm
->mkConst(coef
[pos_var
][0]), newVars
[0]);
2560 Debug("miplib") << "vars[] " << var
<< endl
2561 << " eq " << Rewriter::rewrite(sum
) << endl
;
2562 Node newAssertion
= var
.eqNode(Rewriter::rewrite(sum
));
2563 if(d_topLevelSubstitutions
.hasSubstitution(newAssertion
[0])) {
2564 //Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl;
2565 //Warning() << "REPLACE " << newAssertion[1] << endl;
2566 //Warning() << "ORIG " << d_topLevelSubstitutions.getSubstitution(newAssertion[0]) << endl;
2567 Assert(d_topLevelSubstitutions
.getSubstitution(newAssertion
[0]) == newAssertion
[1]);
2568 } else if(pos
.getNumChildren() <= options::arithMLTrickSubstitutions()) {
2569 d_topLevelSubstitutions
.addSubstitution(newAssertion
[0], newAssertion
[1]);
2570 Debug("miplib") << "addSubs: " << newAssertion
[0] << " to " << newAssertion
[1] << endl
;
2572 Debug("miplib") << "skipSubs: " << newAssertion
[0] << " to " << newAssertion
[1] << " (threshold is " << options::arithMLTrickSubstitutions() << ")" << endl
;
2574 newAssertion
= Rewriter::rewrite(newAssertion
);
2575 Debug("miplib") << " " << newAssertion
<< endl
;
2576 d_assertions
.push_back(newAssertion
);
2577 Debug("miplib") << " assertions to remove: " << endl
;
2578 for(vector
<TNode
>::const_iterator k
= asserts
[pos_var
].begin(), k_end
= asserts
[pos_var
].end(); k
!= k_end
; ++k
) {
2579 Debug("miplib") << " " << *k
<< endl
;
2580 removeAssertions
.insert((*k
).getId());
2586 if(!removeAssertions
.empty()) {
2587 Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl
;
2588 for(size_t i
= 0; i
< d_realAssertionsEnd
; ++i
) {
2589 if(removeAssertions
.find(d_assertions
[i
].getId()) != removeAssertions
.end()) {
2590 Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions
[i
] << endl
;
2591 d_assertions
[i
] = d_true
;
2592 ++d_smt
.d_stats
->d_numMiplibAssertionsRemoved
;
2593 } else if(d_assertions
[i
].getKind() == kind::AND
) {
2594 size_t removals
= removeFromConjunction(d_assertions
[i
], removeAssertions
);
2596 Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions
[i
] << endl
;
2597 Debug("miplib") << "SmtEnginePrivate::simplify(): - by " << removals
<< " conjuncts" << endl
;
2598 d_smt
.d_stats
->d_numMiplibAssertionsRemoved
+= removals
;
2601 Debug("miplib") << "had: " << d_assertions
[i
] << endl
;
2602 d_assertions
[i
] = Rewriter::rewrite(d_topLevelSubstitutions
.apply(d_assertions
[i
]));
2603 Debug("miplib") << "now: " << d_assertions
[i
] << endl
;
2606 Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl
;
2608 d_realAssertionsEnd
= d_assertions
.size();
2612 // returns false if simplification led to "false"
2613 bool SmtEnginePrivate::simplifyAssertions()
2614 throw(TypeCheckingException
, LogicException
) {
2615 Assert(d_smt
.d_pendingPops
== 0);
2617 ScopeCounter
depth(d_simplifyAssertionsDepth
);
2619 Trace("simplify") << "SmtEnginePrivate::simplify()" << endl
;
2621 if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
2622 // Perform non-clausal simplification
2623 Chat() << "...performing nonclausal simplification..." << endl
;
2624 Trace("simplify") << "SmtEnginePrivate::simplify(): "
2625 << "performing non-clausal simplification" << endl
;
2626 bool noConflict
= nonClausalSimplify();
2631 // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
2632 // do the miplib trick.
2633 if( // check that option is on
2634 options::arithMLTrick() &&
2635 // miplib rewrites aren't safe in incremental mode
2636 ! options::incrementalSolving() &&
2637 // only useful in arith
2638 d_smt
.d_logic
.isTheoryEnabled(THEORY_ARITH
) &&
2639 // we add new assertions and need this (in practice, this
2640 // restriction only disables miplib processing during
2641 // re-simplification, which we don't expect to be useful anyway)
2642 d_realAssertionsEnd
== d_assertions
.size() ) {
2643 Chat() << "...fixing miplib encodings..." << endl
;
2644 Trace("simplify") << "SmtEnginePrivate::simplify(): "
2645 << "looking for miplib pseudobooleans..." << endl
;
2647 TimerStat::CodeTimer
miplibTimer(d_smt
.d_stats
->d_miplibPassTime
);
2651 Trace("simplify") << "SmtEnginePrivate::simplify(): "
2652 << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl
;
2656 dumpAssertions("post-nonclausal", d_assertions
);
2657 Trace("smt") << "POST nonClausalSimplify" << endl
;
2658 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2660 // before ppRewrite check if only core theory for BV theory
2661 d_smt
.d_theoryEngine
->staticInitializeBVOptions(d_assertions
.ref());
2663 dumpAssertions("pre-theorypp", d_assertions
);
2665 // Theory preprocessing
2666 if (d_smt
.d_earlyTheoryPP
) {
2667 Chat() << "...doing early theory preprocessing..." << endl
;
2668 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
2669 // Call the theory preprocessors
2670 d_smt
.d_theoryEngine
->preprocessStart();
2671 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2672 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
2673 d_assertions
.replace(i
, d_smt
.d_theoryEngine
->preprocess(d_assertions
[i
]));
2674 Assert(Rewriter::rewrite(d_assertions
[i
]) == d_assertions
[i
]);
2678 dumpAssertions("post-theorypp", d_assertions
);
2679 Trace("smt") << "POST theoryPP" << endl
;
2680 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2682 // ITE simplification
2683 if(options::doITESimp() &&
2684 (d_simplifyAssertionsDepth
<= 1 || options::doITESimpOnRepeat())) {
2685 Chat() << "...doing ITE simplification..." << endl
;
2686 bool noConflict
= simpITE();
2688 Chat() << "...ITE simplification found unsat..." << endl
;
2693 dumpAssertions("post-itesimp", d_assertions
);
2694 Trace("smt") << "POST iteSimp" << endl
;
2695 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2697 // Unconstrained simplification
2698 if(options::unconstrainedSimp()) {
2699 Chat() << "...doing unconstrained simplification..." << endl
;
2700 unconstrainedSimp();
2703 dumpAssertions("post-unconstrained", d_assertions
);
2704 Trace("smt") << "POST unconstrainedSimp" << endl
;
2705 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2707 if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE
) {
2708 Chat() << "...doing another round of nonclausal simplification..." << endl
;
2709 Trace("simplify") << "SmtEnginePrivate::simplify(): "
2710 << " doing repeated simplification" << endl
;
2711 bool noConflict
= nonClausalSimplify();
2717 dumpAssertions("post-repeatsimp", d_assertions
);
2718 Trace("smt") << "POST repeatSimp" << endl
;
2719 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2721 } catch(TypeCheckingExceptionPrivate
& tcep
) {
2722 // Calls to this function should have already weeded out any
2723 // typechecking exceptions via (e.g.) ensureBoolean(). But a
2724 // theory could still create a new expression that isn't
2725 // well-typed, and we don't want the C++ runtime to abort our
2726 // process without any error notice.
2728 ss
<< "A bad expression was produced. Original exception follows:\n"
2730 InternalError(ss
.str().c_str());
2735 Result
SmtEngine::check() {
2736 Assert(d_fullyInited
);
2737 Assert(d_pendingPops
== 0);
2739 Trace("smt") << "SmtEngine::check()" << endl
;
2741 // Make sure the prop layer has all of the assertions
2742 Trace("smt") << "SmtEngine::check(): processing assertions" << endl
;
2743 d_private
->processAssertions();
2745 // Turn off stop only for QF_LRA
2746 // TODO: Bring up in a meeting where to put this
2747 if(options::decisionStopOnly() && !options::decisionMode
.wasSetByUser() ){
2749 (not d_logic
.isQuantified() &&
2750 d_logic
.isPure(THEORY_ARITH
) && d_logic
.isLinear() && !d_logic
.isDifferenceLogic() && !d_logic
.areIntegersUsed()
2752 if(d_private
->d_iteSkolemMap
.empty()){
2753 options::decisionStopOnly
.set(false);
2754 d_decisionEngine
->clearStrategies();
2755 Trace("smt") << "SmtEngine::check(): turning off stop only" << endl
;
2760 unsigned long millis
= 0;
2761 if(d_timeBudgetCumulative
!= 0) {
2762 millis
= getTimeRemaining();
2764 return Result(Result::VALIDITY_UNKNOWN
, Result::TIMEOUT
, d_filename
);
2767 if(d_timeBudgetPerCall
!= 0 && (millis
== 0 || d_timeBudgetPerCall
< millis
)) {
2768 millis
= d_timeBudgetPerCall
;
2771 unsigned long resource
= 0;
2772 if(d_resourceBudgetCumulative
!= 0) {
2773 resource
= getResourceRemaining();
2775 return Result(Result::VALIDITY_UNKNOWN
, Result::RESOURCEOUT
, d_filename
);
2778 if(d_resourceBudgetPerCall
!= 0 && (resource
== 0 || d_resourceBudgetPerCall
< resource
)) {
2779 resource
= d_resourceBudgetPerCall
;
2782 TimerStat::CodeTimer
solveTimer(d_stats
->d_solveTime
);
2784 Chat() << "solving..." << endl
;
2785 Trace("smt") << "SmtEngine::check(): running check" << endl
;
2786 Result result
= d_propEngine
->checkSat(millis
, resource
);
2788 // PropEngine::checkSat() returns the actual amount used in these
2790 d_cumulativeTimeUsed
+= millis
;
2791 d_cumulativeResourceUsed
+= resource
;
2793 Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
2794 << ", conflicts " << d_cumulativeResourceUsed
<< endl
;
2796 return Result(result
, d_filename
);
2799 Result
SmtEngine::quickCheck() {
2800 Assert(d_fullyInited
);
2801 Trace("smt") << "SMT quickCheck()" << endl
;
2802 return Result(Result::VALIDITY_UNKNOWN
, Result::REQUIRES_FULL_CHECK
, d_filename
);
2806 void SmtEnginePrivate::collectSkolems(TNode n
, set
<TNode
>& skolemSet
, hash_map
<Node
, bool, NodeHashFunction
>& cache
)
2808 hash_map
<Node
, bool, NodeHashFunction
>::iterator it
;
2810 if (it
!= cache
.end()) {
2814 size_t sz
= n
.getNumChildren();
2816 IteSkolemMap::iterator it
= d_iteSkolemMap
.find(n
);
2817 if (it
!= d_iteSkolemMap
.end()) {
2818 skolemSet
.insert(n
);
2825 for (; k
< sz
; ++k
) {
2826 collectSkolems(n
[k
], skolemSet
, cache
);
2832 bool SmtEnginePrivate::checkForBadSkolems(TNode n
, TNode skolem
, hash_map
<Node
, bool, NodeHashFunction
>& cache
)
2834 hash_map
<Node
, bool, NodeHashFunction
>::iterator it
;
2836 if (it
!= cache
.end()) {
2837 return (*it
).second
;
2840 size_t sz
= n
.getNumChildren();
2842 IteSkolemMap::iterator it
= d_iteSkolemMap
.find(n
);
2844 if (it
!= d_iteSkolemMap
.end()) {
2845 if (!((*it
).first
< n
)) {
2854 for (; k
< sz
; ++k
) {
2855 if (checkForBadSkolems(n
[k
], skolem
, cache
)) {
2865 Node
SmtEnginePrivate::rewriteBooleanTerms(TNode n
) {
2866 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_rewriteBooleanTermsTime
);
2867 if(d_booleanTermConverter
== NULL
) {
2868 // This needs to be initialized _after_ the whole SMT framework is in place, subscribed
2869 // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype
2870 // definition, and not dump it properly.
2871 d_booleanTermConverter
= new BooleanTermConverter(d_smt
);
2873 Node retval
= d_booleanTermConverter
->rewriteBooleanTerms(n
);
2875 switch(booleans::BooleanTermConversionMode mode
= options::booleanTermConversionMode()) {
2876 case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS
:
2877 case booleans::BOOLEAN_TERM_CONVERT_NATIVE
:
2878 if(!d_smt
.d_logic
.isTheoryEnabled(THEORY_BV
)) {
2879 d_smt
.d_logic
= d_smt
.d_logic
.getUnlockedCopy();
2880 d_smt
.d_logic
.enableTheory(THEORY_BV
);
2881 d_smt
.d_logic
.lock();
2884 case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES
:
2885 if(!d_smt
.d_logic
.isTheoryEnabled(THEORY_DATATYPES
)) {
2886 d_smt
.d_logic
= d_smt
.d_logic
.getUnlockedCopy();
2887 d_smt
.d_logic
.enableTheory(THEORY_DATATYPES
);
2888 d_smt
.d_logic
.lock();
2898 void SmtEnginePrivate::processAssertions() {
2899 TimerStat::CodeTimer
paTimer(d_smt
.d_stats
->d_processAssertionsTime
);
2901 Assert(d_smt
.d_fullyInited
);
2902 Assert(d_smt
.d_pendingPops
== 0);
2904 // Dump the assertions
2905 dumpAssertions("pre-everything", d_assertions
);
2907 Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl
;
2909 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2911 if (d_assertions
.size() == 0) {
2916 if (d_assertionsProcessed
&& options::incrementalSolving()) {
2917 // Placeholder for storing substitutions
2918 d_substitutionsIndex
= d_assertions
.size();
2919 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
2922 // Add dummy assertion in last position - to be used as a
2923 // placeholder for any new assertions to get added
2924 d_assertions
.push_back(NodeManager::currentNM()->mkConst
<bool>(true));
2925 // any assertions added beyond realAssertionsEnd must NOT affect the
2926 // equisatisfiability
2927 d_realAssertionsEnd
= d_assertions
.size();
2929 // Assertions are NOT guaranteed to be rewritten by this point
2931 dumpAssertions("pre-definition-expansion", d_assertions
);
2933 Chat() << "expanding definitions..." << endl
;
2934 Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl
;
2935 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_definitionExpansionTime
);
2936 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
2937 for(unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
2938 d_assertions
.replace(i
, expandDefinitions(d_assertions
[i
], cache
));
2941 dumpAssertions("post-definition-expansion", d_assertions
);
2943 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2945 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&&
2946 !d_smt
.d_logic
.isPure(THEORY_BV
)) {
2947 throw ModalException("Eager bit-blasting does not currently support theory combination. "
2948 "Note that in a QF_BV problem UF symbols can be introduced for division. "
2949 "Try --bv-div-zero-const to interpret division by zero as a constant.");
2952 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
2953 d_smt
.d_theoryEngine
->mkAckermanizationAsssertions(d_assertions
.ref());
2956 if ( options::bvAbstraction() &&
2957 !options::incrementalSolving()) {
2958 dumpAssertions("pre-bv-abstraction", d_assertions
);
2960 dumpAssertions("post-bv-abstraction", d_assertions
);
2963 dumpAssertions("pre-boolean-terms", d_assertions
);
2965 Chat() << "rewriting Boolean terms..." << endl
;
2966 for(unsigned i
= 0, i_end
= d_assertions
.size(); i
!= i_end
; ++i
) {
2967 d_assertions
.replace(i
, rewriteBooleanTerms(d_assertions
[i
]));
2970 dumpAssertions("post-boolean-terms", d_assertions
);
2972 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2974 dumpAssertions("pre-constrain-subtypes", d_assertions
);
2976 // Any variables of subtype types need to be constrained properly.
2977 // Careful, here: constrainSubtypes() adds to the back of
2978 // d_assertions, but we don't need to reprocess those.
2979 // We also can't use an iterator, because the vector may be moved in
2980 // memory during this loop.
2981 Chat() << "constraining subtypes..." << endl
;
2982 for(unsigned i
= 0, i_end
= d_assertions
.size(); i
!= i_end
; ++i
) {
2983 constrainSubtypes(d_assertions
[i
], d_assertions
);
2986 dumpAssertions("post-constrain-subtypes", d_assertions
);
2988 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
2990 bool noConflict
= true;
2992 // Unconstrained simplification
2993 if(options::unconstrainedSimp()) {
2994 dumpAssertions("pre-unconstrained-simp", d_assertions
);
2995 Chat() << "...doing unconstrained simplification..." << endl
;
2996 unconstrainedSimp();
2997 dumpAssertions("post-unconstrained-simp", d_assertions
);
3000 if(options::bvIntroducePow2()){
3001 theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions
.ref());
3004 dumpAssertions("pre-substitution", d_assertions
);
3006 if(options::unsatCores()) {
3007 // special rewriting pass for unsat cores, since many of the passes below are skipped
3008 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3009 d_assertions
.replace(i
, Rewriter::rewrite(d_assertions
[i
]));
3012 // Apply the substitutions we already have, and normalize
3013 if(!options::unsatCores()) {
3014 Chat() << "applying substitutions..." << endl
;
3015 Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3016 << "applying substitutions" << endl
;
3017 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3018 Trace("simplify") << "applying to " << d_assertions
[i
] << endl
;
3019 d_assertions
.replace(i
, Rewriter::rewrite(d_topLevelSubstitutions
.apply(d_assertions
[i
])));
3020 Trace("simplify") << " got " << d_assertions
[i
] << endl
;
3025 dumpAssertions("post-substitution", d_assertions
);
3027 // Assertions ARE guaranteed to be rewritten by this point
3029 // Lift bit-vectors of size 1 to bool
3030 if(options::bitvectorToBool()) {
3031 dumpAssertions("pre-bv-to-bool", d_assertions
);
3032 Chat() << "...doing bvToBool..." << endl
;
3034 dumpAssertions("post-bv-to-bool", d_assertions
);
3037 if( d_smt
.d_logic
.isTheoryEnabled(THEORY_STRINGS
) ) {
3038 dumpAssertions("pre-strings-pp", d_assertions
);
3039 CVC4::theory::strings::StringsPreprocess sp
;
3040 std::vector
<Node
> newNodes
;
3041 newNodes
.push_back(d_assertions
[d_realAssertionsEnd
- 1]);
3042 sp
.simplify( d_assertions
.ref(), newNodes
);
3043 if(newNodes
.size() > 1) {
3044 d_assertions
[d_realAssertionsEnd
- 1] = NodeManager::currentNM()->mkNode(kind::AND
, newNodes
);
3046 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3047 d_assertions
[i
] = Rewriter::rewrite( d_assertions
[i
] );
3049 dumpAssertions("post-strings-pp", d_assertions
);
3051 if( d_smt
.d_logic
.isQuantified() ){
3052 //remove rewrite rules
3053 for( unsigned i
=0; i
< d_assertions
.size(); i
++ ) {
3054 if( d_assertions
[i
].getKind() == kind::REWRITE_RULE
){
3055 Node prev
= d_assertions
[i
];
3056 Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev
<< "..." << std::endl
;
3057 d_assertions
[i
] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions
[i
] ) );
3058 Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev
<< endl
;
3059 Trace("quantifiers-rewrite") << " ...got " << d_assertions
[i
] << endl
;
3063 dumpAssertions("pre-skolem-quant", d_assertions
);
3064 if( options::preSkolemQuant() ){
3065 //apply pre-skolemization to existential quantifiers
3066 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3067 Node prev
= d_assertions
[i
];
3068 Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev
<< "..." << std::endl
;
3069 vector
< TypeNode
> fvTypes
;
3070 vector
< TNode
> fvs
;
3071 d_assertions
.replace(i
, quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev
, true, fvTypes
, fvs
));
3072 if( prev
!=d_assertions
[i
] ){
3073 d_assertions
.replace(i
, Rewriter::rewrite( d_assertions
[i
] ));
3074 Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev
<< endl
;
3075 Trace("quantifiers-rewrite") << " ...got " << d_assertions
[i
] << endl
;
3079 dumpAssertions("post-skolem-quant", d_assertions
);
3080 if( options::macrosQuant() ){
3081 //quantifiers macro expansion
3084 quantifiers::QuantifierMacros qm
;
3085 success
= qm
.simplify( d_assertions
.ref(), true );
3089 Trace("fo-rsn-enable") << std::endl
;
3090 if( options::foPropQuant() ){
3091 quantifiers::FirstOrderPropagation fop
;
3092 fop
.simplify( d_assertions
.ref() );
3096 if( options::sortInference() ){
3097 //sort inference technique
3098 SortInference
* si
= d_smt
.d_theoryEngine
->getSortInference();
3099 si
->simplify( d_assertions
.ref() );
3100 for( std::map
< Node
, Node
>::iterator it
= si
->d_model_replace_f
.begin(); it
!= si
->d_model_replace_f
.end(); ++it
){
3101 d_smt
.setPrintFuncInModel( it
->first
.toExpr(), false );
3102 d_smt
.setPrintFuncInModel( it
->second
.toExpr(), true );
3106 //if( options::quantConflictFind() ){
3107 // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertions );
3110 if( options::pbRewrites() ){
3111 d_pbsProcessor
.learn(d_assertions
.ref());
3112 if(d_pbsProcessor
.likelyToHelp()){
3113 d_pbsProcessor
.applyReplacements(d_assertions
.ref());
3117 dumpAssertions("pre-simplify", d_assertions
);
3118 Chat() << "simplifying assertions..." << endl
;
3119 noConflict
= simplifyAssertions();
3121 ++(d_smt
.d_stats
->d_simplifiedToFalse
);
3123 dumpAssertions("post-simplify", d_assertions
);
3125 dumpAssertions("pre-static-learning", d_assertions
);
3126 if(options::doStaticLearning()) {
3127 // Perform static learning
3128 Chat() << "doing static learning..." << endl
;
3129 Trace("simplify") << "SmtEnginePrivate::simplify(): "
3130 << "performing static learning" << endl
;
3133 dumpAssertions("post-static-learning", d_assertions
);
3135 Trace("smt") << "POST bvToBool" << endl
;
3136 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3139 dumpAssertions("pre-ite-removal", d_assertions
);
3141 Chat() << "removing term ITEs..." << endl
;
3142 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_iteRemovalTime
);
3143 // Remove ITEs, updating d_iteSkolemMap
3144 d_smt
.d_stats
->d_numAssertionsPre
+= d_assertions
.size();
3146 d_smt
.d_stats
->d_numAssertionsPost
+= d_assertions
.size();
3148 dumpAssertions("post-ite-removal", d_assertions
);
3150 dumpAssertions("pre-repeat-simplify", d_assertions
);
3151 if(options::repeatSimp()) {
3152 Chat() << "re-simplifying assertions..." << endl
;
3153 ScopeCounter
depth(d_simplifyAssertionsDepth
);
3154 noConflict
&= simplifyAssertions();
3156 // Need to fix up assertion list to maintain invariants:
3157 // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be the order in which these variables were introduced
3158 // during ite removal.
3159 // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
3161 // cache for expression traversal
3162 hash_map
<Node
, bool, NodeHashFunction
> cache
;
3164 // First, find all skolems that appear in the substitution map - their associated iteExpr will need
3165 // to be moved to the main assertion set
3166 set
<TNode
> skolemSet
;
3167 SubstitutionMap::iterator pos
= d_topLevelSubstitutions
.begin();
3168 for (; pos
!= d_topLevelSubstitutions
.end(); ++pos
) {
3169 collectSkolems((*pos
).first
, skolemSet
, cache
);
3170 collectSkolems((*pos
).second
, skolemSet
, cache
);
3173 // We need to ensure:
3174 // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
3175 // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
3176 // If either of these is violated, we must add iteExpr as a proper assertion
3177 IteSkolemMap::iterator it
= d_iteSkolemMap
.begin();
3178 IteSkolemMap::iterator iend
= d_iteSkolemMap
.end();
3179 NodeBuilder
<> builder(kind::AND
);
3180 builder
<< d_assertions
[d_realAssertionsEnd
- 1];
3181 vector
<TNode
> toErase
;
3182 for (; it
!= iend
; ++it
) {
3183 if (skolemSet
.find((*it
).first
) == skolemSet
.end()) {
3184 TNode iteExpr
= d_assertions
[(*it
).second
];
3185 if (iteExpr
.getKind() == kind::ITE
&&
3186 iteExpr
[1].getKind() == kind::EQUAL
&&
3187 iteExpr
[1][0] == (*it
).first
&&
3188 iteExpr
[2].getKind() == kind::EQUAL
&&
3189 iteExpr
[2][0] == (*it
).first
) {
3191 bool bad
= checkForBadSkolems(iteExpr
[0], (*it
).first
, cache
);
3192 bad
= bad
|| checkForBadSkolems(iteExpr
[1][1], (*it
).first
, cache
);
3193 bad
= bad
|| checkForBadSkolems(iteExpr
[2][1], (*it
).first
, cache
);
3199 // Move this iteExpr into the main assertions
3200 builder
<< d_assertions
[(*it
).second
];
3201 d_assertions
[(*it
).second
] = NodeManager::currentNM()->mkConst
<bool>(true);
3202 toErase
.push_back((*it
).first
);
3204 if(builder
.getNumChildren() > 1) {
3205 while (!toErase
.empty()) {
3206 d_iteSkolemMap
.erase(toErase
.back());
3209 d_assertions
[d_realAssertionsEnd
- 1] =
3210 Rewriter::rewrite(Node(builder
));
3212 // For some reason this is needed for some benchmarks, such as
3213 // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
3214 // Figure it out later
3216 // Assert(iteRewriteAssertionsEnd == d_assertions.size());
3219 dumpAssertions("post-repeat-simplify", d_assertions
);
3221 dumpAssertions("pre-rewrite-apply-to-const", d_assertions
);
3222 if(options::rewriteApplyToConst()) {
3223 Chat() << "Rewriting applies to constants..." << endl
;
3224 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_rewriteApplyToConstTime
);
3225 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3226 d_assertions
[i
] = Rewriter::rewrite(rewriteApplyToConst(d_assertions
[i
]));
3229 dumpAssertions("post-rewrite-apply-to-const", d_assertions
);
3231 // begin: INVARIANT to maintain: no reordering of assertions or
3232 // introducing new ones
3233 #ifdef CVC4_ASSERTIONS
3234 unsigned iteRewriteAssertionsEnd
= d_assertions
.size();
3237 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3239 Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl
;
3240 Debug("smt") << " d_assertions : " << d_assertions
.size() << endl
;
3242 dumpAssertions("pre-theory-preprocessing", d_assertions
);
3244 Chat() << "theory preprocessing..." << endl
;
3245 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_theoryPreprocessTime
);
3246 // Call the theory preprocessors
3247 d_smt
.d_theoryEngine
->preprocessStart();
3248 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3249 d_assertions
.replace(i
, d_smt
.d_theoryEngine
->preprocess(d_assertions
[i
]));
3252 dumpAssertions("post-theory-preprocessing", d_assertions
);
3254 // If we are using eager bit-blasting wrap assertions in fake atom so that
3255 // everything gets bit-blasted to internal SAT solver
3256 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
3257 for (unsigned i
= 0; i
< d_assertions
.size(); ++i
) {
3258 TNode atom
= d_assertions
[i
];
3259 Node eager_atom
= NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM
, atom
);
3260 d_assertions
.replace(i
, eager_atom
);
3261 TheoryModel
* m
= d_smt
.d_theoryEngine
->getModel();
3262 m
->addSubstitution(eager_atom
, atom
);
3266 // Push the formula to decision engine
3268 Chat() << "pushing to decision engine..." << endl
;
3269 Assert(iteRewriteAssertionsEnd
== d_assertions
.size());
3270 d_smt
.d_decisionEngine
->addAssertions
3271 (d_assertions
.ref(), d_realAssertionsEnd
, d_iteSkolemMap
);
3274 // end: INVARIANT to maintain: no reordering of assertions or
3275 // introducing new ones
3277 dumpAssertions("post-everything", d_assertions
);
3279 //set instantiation level of everything to zero
3280 if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
3281 for( unsigned i
=0; i
< d_assertions
.size(); i
++ ) {
3282 theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertions
[i
], 0 );
3286 // Push the formula to SAT
3288 Chat() << "converting to CNF..." << endl
;
3289 TimerStat::CodeTimer
codeTimer(d_smt
.d_stats
->d_cnfConversionTime
);
3290 for (unsigned i
= 0; i
< d_assertions
.size(); ++ i
) {
3291 Chat() << "+ " << d_assertions
[i
] << std::endl
;
3292 d_smt
.d_propEngine
->assertFormula(d_assertions
[i
]);
3296 d_assertionsProcessed
= true;
3298 d_assertions
.clear();
3299 d_iteSkolemMap
.clear();
3302 void SmtEnginePrivate::addFormula(TNode n
)
3303 throw(TypeCheckingException
, LogicException
) {
3310 Trace("smt") << "SmtEnginePrivate::addFormula(" << n
<< ")" << endl
;
3312 // Add the normalized formula to the queue
3313 d_assertions
.push_back(n
);
3314 //d_assertions.push_back(Rewriter::rewrite(n));
3317 void SmtEngine::ensureBoolean(const Expr
& e
) throw(TypeCheckingException
) {
3318 Type type
= e
.getType(options::typeChecking());
3319 Type boolType
= d_exprManager
->booleanType();
3320 if(type
!= boolType
) {
3322 ss
<< "Expected " << boolType
<< "\n"
3323 << "The assertion : " << e
<< "\n"
3324 << "Its type : " << type
;
3325 throw TypeCheckingException(e
, ss
.str());
3329 Result
SmtEngine::checkSat(const Expr
& ex
, bool inUnsatCore
) throw(TypeCheckingException
, ModalException
, LogicException
) {
3330 Assert(ex
.isNull() || ex
.getExprManager() == d_exprManager
);
3331 SmtScope
smts(this);
3332 finalOptionsAreSet();
3335 Trace("smt") << "SmtEngine::checkSat(" << ex
<< ")" << endl
;
3337 if(d_queryMade
&& !options::incrementalSolving()) {
3338 throw ModalException("Cannot make multiple queries unless "
3339 "incremental solving is enabled "
3340 "(try --incremental)");
3345 // Substitute out any abstract values in ex.
3346 e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3347 // Ensure expr is type-checked at this point.
3349 // Give it to proof manager
3350 PROOF( ProofManager::currentPM()->addAssertion(e
, inUnsatCore
); );
3353 // check to see if a postsolve() is pending
3354 if(d_needPostsolve
) {
3355 d_theoryEngine
->postsolve();
3356 d_needPostsolve
= false;
3362 // Note that a query has been made
3367 d_problemExtended
= true;
3368 if(d_assertionList
!= NULL
) {
3369 d_assertionList
->push_back(e
);
3371 d_private
->addFormula(e
.getNode());
3375 Result r
= check().asSatisfiabilityResult();
3376 d_needPostsolve
= true;
3378 // Dump the query if requested
3379 if(Dump
.isOn("benchmark")) {
3380 // the expr already got dumped out if assertion-dumping is on
3381 Dump("benchmark") << CheckSatCommand();
3387 // Remember the status
3390 d_problemExtended
= false;
3392 Trace("smt") << "SmtEngine::checkSat(" << e
<< ") => " << r
<< endl
;
3394 // Check that SAT results generate a model correctly.
3395 if(options::checkModels()) {
3396 if(r
.asSatisfiabilityResult().isSat() == Result::SAT
||
3397 (r
.isUnknown() && r
.whyUnknown() == Result::INCOMPLETE
) ){
3398 checkModel(/* hard failure iff */ ! r
.isUnknown());
3401 // Check that UNSAT results generate a proof correctly.
3402 if(options::checkProofs()) {
3403 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
3404 TimerStat::CodeTimer
checkProofTimer(d_stats
->d_checkProofTime
);
3410 }/* SmtEngine::checkSat() */
3412 Result
SmtEngine::query(const Expr
& ex
, bool inUnsatCore
) throw(TypeCheckingException
, ModalException
, LogicException
) {
3413 Assert(!ex
.isNull());
3414 Assert(ex
.getExprManager() == d_exprManager
);
3415 SmtScope
smts(this);
3416 finalOptionsAreSet();
3418 Trace("smt") << "SMT query(" << ex
<< ")" << endl
;
3420 if(d_queryMade
&& !options::incrementalSolving()) {
3421 throw ModalException("Cannot make multiple queries unless "
3422 "incremental solving is enabled "
3423 "(try --incremental)");
3426 // Substitute out any abstract values in ex
3427 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3428 // Ensure that the expression is type-checked at this point, and Boolean
3430 // Give it to proof manager
3431 PROOF( ProofManager::currentPM()->addAssertion(e
.notExpr(), inUnsatCore
); );
3433 // check to see if a postsolve() is pending
3434 if(d_needPostsolve
) {
3435 d_theoryEngine
->postsolve();
3436 d_needPostsolve
= false;
3442 // Note that a query has been made
3446 d_problemExtended
= true;
3447 if(d_assertionList
!= NULL
) {
3448 d_assertionList
->push_back(e
.notExpr());
3450 d_private
->addFormula(e
.getNode().notNode());
3453 Result r
= check().asValidityResult();
3454 d_needPostsolve
= true;
3456 // Dump the query if requested
3457 if(Dump
.isOn("benchmark")) {
3458 // the expr already got dumped out if assertion-dumping is on
3459 Dump("benchmark") << CheckSatCommand();
3465 // Remember the status
3468 d_problemExtended
= false;
3470 Trace("smt") << "SMT query(" << e
<< ") ==> " << r
<< endl
;
3472 // Check that SAT results generate a model correctly.
3473 if(options::checkModels()) {
3474 if(r
.asSatisfiabilityResult().isSat() == Result::SAT
||
3475 (r
.isUnknown() && r
.whyUnknown() == Result::INCOMPLETE
) ){
3476 checkModel(/* hard failure iff */ ! r
.isUnknown());
3479 // Check that UNSAT results generate a proof correctly.
3480 if(options::checkProofs()) {
3481 if(r
.asSatisfiabilityResult().isSat() == Result::UNSAT
) {
3482 TimerStat::CodeTimer
checkProofTimer(d_stats
->d_checkProofTime
);
3488 }/* SmtEngine::query() */
3490 Result
SmtEngine::assertFormula(const Expr
& ex
, bool inUnsatCore
) throw(TypeCheckingException
, LogicException
) {
3491 Assert(ex
.getExprManager() == d_exprManager
);
3492 SmtScope
smts(this);
3493 finalOptionsAreSet();
3496 PROOF( ProofManager::currentPM()->addAssertion(ex
, inUnsatCore
); );
3498 Trace("smt") << "SmtEngine::assertFormula(" << ex
<< ")" << endl
;
3500 // Substitute out any abstract values in ex
3501 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3504 if(d_assertionList
!= NULL
) {
3505 d_assertionList
->push_back(e
);
3507 d_private
->addFormula(e
.getNode());
3508 return quickCheck().asValidityResult();
3509 }/* SmtEngine::assertFormula() */
3511 Node
SmtEngine::postprocess(TNode node
, TypeNode expectedType
) const {
3512 ModelPostprocessor mpost
;
3513 NodeVisitor
<ModelPostprocessor
> visitor
;
3514 Node value
= visitor
.run(mpost
, node
);
3515 Debug("boolean-terms") << "postproc: got " << value
<< " expect type " << expectedType
<< endl
;
3516 Node realValue
= mpost
.rewriteAs(value
, expectedType
);
3517 Debug("boolean-terms") << "postproc: realval " << realValue
<< " expect type " << expectedType
<< endl
;
3521 Expr
SmtEngine::simplify(const Expr
& ex
) throw(TypeCheckingException
, LogicException
) {
3522 Assert(ex
.getExprManager() == d_exprManager
);
3523 SmtScope
smts(this);
3524 finalOptionsAreSet();
3526 Trace("smt") << "SMT simplify(" << ex
<< ")" << endl
;
3528 if(Dump
.isOn("benchmark")) {
3529 Dump("benchmark") << SimplifyCommand(ex
);
3532 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3533 if( options::typeChecking() ) {
3534 e
.getType(true); // ensure expr is type-checked at this point
3537 // Make sure all preprocessing is done
3538 d_private
->processAssertions();
3539 Node n
= d_private
->simplify(Node::fromExpr(e
));
3540 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
3544 Expr
SmtEngine::expandDefinitions(const Expr
& ex
) throw(TypeCheckingException
, LogicException
) {
3545 Assert(ex
.getExprManager() == d_exprManager
);
3546 SmtScope
smts(this);
3547 finalOptionsAreSet();
3549 Trace("smt") << "SMT expandDefinitions(" << ex
<< ")" << endl
;
3551 // Substitute out any abstract values in ex.
3552 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3553 if(options::typeChecking()) {
3554 // Ensure expr is type-checked at this point.
3557 if(Dump
.isOn("benchmark")) {
3558 Dump("benchmark") << ExpandDefinitionsCommand(e
);
3560 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
3561 Node n
= d_private
->expandDefinitions(Node::fromExpr(e
), cache
, /* expandOnly = */ true);
3562 n
= postprocess(n
, TypeNode::fromType(e
.getType()));
3567 Expr
SmtEngine::getValue(const Expr
& ex
) const throw(ModalException
, TypeCheckingException
, LogicException
) {
3568 Assert(ex
.getExprManager() == d_exprManager
);
3569 SmtScope
smts(this);
3571 Trace("smt") << "SMT getValue(" << ex
<< ")" << endl
;
3572 if(Dump
.isOn("benchmark")) {
3573 Dump("benchmark") << GetValueCommand(ex
);
3576 if(!options::produceModels()) {
3578 "Cannot get value when produce-models options is off.";
3579 throw ModalException(msg
);
3581 if(d_status
.isNull() ||
3582 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
3583 d_problemExtended
) {
3585 "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
3586 throw ModalException(msg
);
3589 // Substitute out any abstract values in ex.
3590 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3592 // Ensure expr is type-checked at this point.
3593 e
.getType(options::typeChecking());
3595 // do not need to apply preprocessing substitutions (should be recorded
3596 // in model already)
3598 Node n
= Node::fromExpr(e
);
3599 Trace("smt") << "--- getting value of " << n
<< endl
;
3600 TypeNode expectedType
= n
.getType();
3602 // Expand, then normalize
3603 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
3604 n
= d_private
->expandDefinitions(n
, cache
);
3605 // There are two ways model values for terms are computed (for historical
3606 // reasons). One way is that used in check-model; the other is that
3607 // used by the Model classes. It's not clear to me exactly how these
3608 // two are different, but they need to be unified. This ugly hack here
3609 // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
3610 if(!n
.getType().isFunction()) {
3611 n
= d_private
->rewriteBooleanTerms(n
);
3612 n
= Rewriter::rewrite(n
);
3615 Trace("smt") << "--- getting value of " << n
<< endl
;
3616 TheoryModel
* m
= d_theoryEngine
->getModel();
3619 resultNode
= m
->getValue(n
);
3621 Trace("smt") << "--- got value " << n
<< " = " << resultNode
<< endl
;
3622 resultNode
= postprocess(resultNode
, expectedType
);
3623 Trace("smt") << "--- model-post returned " << resultNode
<< endl
;
3624 Trace("smt") << "--- model-post returned " << resultNode
.getType() << endl
;
3625 Trace("smt") << "--- model-post expected " << expectedType
<< endl
;
3627 // type-check the result we got
3628 Assert(resultNode
.isNull() || resultNode
.getType().isSubtypeOf(expectedType
),
3629 "Run with -t smt for details.");
3631 // ensure it's a constant
3632 Assert(resultNode
.getKind() == kind::LAMBDA
|| resultNode
.isConst());
3634 if(options::abstractValues() && resultNode
.getType().isArray()) {
3635 resultNode
= d_private
->mkAbstractValue(resultNode
);
3638 return resultNode
.toExpr();
3641 bool SmtEngine::addToAssignment(const Expr
& ex
) throw() {
3642 SmtScope
smts(this);
3643 finalOptionsAreSet();
3645 // Substitute out any abstract values in ex
3646 Expr e
= d_private
->substituteAbstractValues(Node::fromExpr(ex
)).toExpr();
3647 Type type
= e
.getType(options::typeChecking());
3649 CheckArgument( type
.isBoolean(), e
,
3650 "expected Boolean-typed variable or function application "
3651 "in addToAssignment()" );
3652 Node n
= e
.getNode();
3653 // must be an APPLY of a zero-ary defined function, or a variable
3654 CheckArgument( ( ( n
.getKind() == kind::APPLY
&&
3655 ( d_definedFunctions
->find(n
.getOperator()) !=
3656 d_definedFunctions
->end() ) &&
3657 n
.getNumChildren() == 0 ) ||
3659 "expected variable or defined-function application "
3660 "in addToAssignment(),\ngot %s", e
.toString().c_str() );
3661 if(!options::produceAssignments()) {
3664 if(d_assignments
== NULL
) {
3665 d_assignments
= new(true) AssignmentSet(d_context
);
3667 d_assignments
->insert(n
);
3672 CVC4::SExpr
SmtEngine::getAssignment() throw(ModalException
) {
3673 Trace("smt") << "SMT getAssignment()" << endl
;
3674 SmtScope
smts(this);
3675 finalOptionsAreSet();
3676 if(Dump
.isOn("benchmark")) {
3677 Dump("benchmark") << GetAssignmentCommand();
3679 if(!options::produceAssignments()) {
3681 "Cannot get the current assignment when "
3682 "produce-assignments option is off.";
3683 throw ModalException(msg
);
3685 if(d_status
.isNull() ||
3686 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
3687 d_problemExtended
) {
3689 "Cannot get the current assignment unless immediately "
3690 "preceded by SAT/INVALID or UNKNOWN response.";
3691 throw ModalException(msg
);
3694 if(d_assignments
== NULL
) {
3695 return SExpr(vector
<SExpr
>());
3698 vector
<SExpr
> sexprs
;
3699 TypeNode boolType
= d_nodeManager
->booleanType();
3700 TheoryModel
* m
= d_theoryEngine
->getModel();
3701 for(AssignmentSet::const_iterator i
= d_assignments
->begin(),
3702 iend
= d_assignments
->end();
3705 Assert((*i
).getType() == boolType
);
3707 Trace("smt") << "--- getting value of " << *i
<< endl
;
3709 // Expand, then normalize
3710 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
3711 Node n
= d_private
->expandDefinitions(*i
, cache
);
3712 n
= d_private
->rewriteBooleanTerms(n
);
3713 n
= Rewriter::rewrite(n
);
3715 Trace("smt") << "--- getting value of " << n
<< endl
;
3718 resultNode
= m
->getValue(n
);
3721 // type-check the result we got
3722 Assert(resultNode
.isNull() || resultNode
.getType() == boolType
);
3724 // ensure it's a constant
3725 Assert(resultNode
.isConst());
3728 if((*i
).getKind() == kind::APPLY
) {
3729 Assert((*i
).getNumChildren() == 0);
3730 v
.push_back(SExpr::Keyword((*i
).getOperator().toString()));
3732 Assert((*i
).isVar());
3733 v
.push_back(SExpr::Keyword((*i
).toString()));
3735 v
.push_back(SExpr::Keyword(resultNode
.toString()));
3736 sexprs
.push_back(v
);
3738 return SExpr(sexprs
);
3741 void SmtEngine::addToModelCommandAndDump(const Command
& c
, uint32_t flags
, bool userVisible
, const char* dumpTag
) {
3742 Trace("smt") << "SMT addToModelCommandAndDump(" << c
<< ")" << endl
;
3743 SmtScope
smts(this);
3744 // If we aren't yet fully inited, the user might still turn on
3745 // produce-models. So let's keep any commands around just in
3746 // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
3747 // sort "U" in QF_UF before setLogic() is run and we still want to
3748 // support finding card(U) with --finite-model-find, and (2) to
3749 // decouple SmtEngine and ExprManager if the user does a few
3750 // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
3751 // and expects to find their cardinalities in the model.
3752 if(/* userVisible && */
3753 (!d_fullyInited
|| options::produceModels()) &&
3754 (flags
& ExprManager::VAR_FLAG_DEFINED
) == 0) {
3756 if(flags
& ExprManager::VAR_FLAG_GLOBAL
) {
3757 d_modelGlobalCommands
.push_back(c
.clone());
3759 d_modelCommands
->push_back(c
.clone());
3762 if(Dump
.isOn(dumpTag
)) {
3766 d_dumpCommands
.push_back(c
.clone());
3771 Model
* SmtEngine::getModel() throw(ModalException
) {
3772 Trace("smt") << "SMT getModel()" << endl
;
3773 SmtScope
smts(this);
3775 finalOptionsAreSet();
3777 if(Dump
.isOn("benchmark")) {
3778 Dump("benchmark") << GetModelCommand();
3781 if(d_status
.isNull() ||
3782 d_status
.asSatisfiabilityResult() == Result::UNSAT
||
3783 d_problemExtended
) {
3785 "Cannot get the current model unless immediately "
3786 "preceded by SAT/INVALID or UNKNOWN response.";
3787 throw ModalException(msg
);
3789 if(!options::produceModels()) {
3791 "Cannot get model when produce-models options is off.";
3792 throw ModalException(msg
);
3794 TheoryModel
* m
= d_theoryEngine
->getModel();
3795 m
->d_inputName
= d_filename
;
3799 void SmtEngine::checkModel(bool hardFailure
) {
3800 // --check-model implies --interactive, which enables the assertion list,
3801 // so we should be ok.
3802 Assert(d_assertionList
!= NULL
, "don't have an assertion list to check in SmtEngine::checkModel()");
3804 TimerStat::CodeTimer
checkModelTimer(d_stats
->d_checkModelTime
);
3806 // Throughout, we use Notice() to give diagnostic output.
3808 // If this function is running, the user gave --check-model (or equivalent),
3809 // and if Notice() is on, the user gave --verbose (or equivalent).
3811 Notice() << "SmtEngine::checkModel(): generating model" << endl
;
3812 TheoryModel
* m
= d_theoryEngine
->getModel();
3814 // Check individual theory assertions
3815 d_theoryEngine
->checkTheoryAssertionsWithModel();
3820 // We have a "fake context" for the substitution map (we don't need it
3821 // to be context-dependent)
3822 context::Context fakeContext
;
3823 SubstitutionMap
substitutions(&fakeContext
, /* substituteUnderQuantifiers = */ false);
3825 for(size_t k
= 0; k
< m
->getNumCommands(); ++k
) {
3826 const DeclareFunctionCommand
* c
= dynamic_cast<const DeclareFunctionCommand
*>(m
->getCommand(k
));
3827 Notice() << "SmtEngine::checkModel(): model command " << k
<< " : " << m
->getCommand(k
) << endl
;
3829 // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
3830 Notice() << "SmtEngine::checkModel(): skipping..." << endl
;
3832 // We have a DECLARE-FUN:
3834 // We'll first do some checks, then add to our substitution map
3835 // the mapping: function symbol |-> value
3837 Expr func
= c
->getFunction();
3838 Node val
= m
->getValue(func
);
3840 Notice() << "SmtEngine::checkModel(): adding substitution: " << func
<< " |-> " << val
<< endl
;
3842 // (1) if the value is a lambda, ensure the lambda doesn't contain the
3843 // function symbol (since then the definition is recursive)
3844 if (val
.getKind() == kind::LAMBDA
) {
3845 // first apply the model substitutions we have so far
3846 Debug("boolean-terms") << "applying subses to " << val
[1] << endl
;
3847 Node n
= substitutions
.apply(val
[1]);
3848 Debug("boolean-terms") << "++ got " << n
<< endl
;
3849 // now check if n contains func by doing a substitution
3850 // [func->func2] and checking equality of the Nodes.
3851 // (this just a way to check if func is in n.)
3852 SubstitutionMap
subs(&fakeContext
);
3853 Node func2
= NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func
.getType()), "", NodeManager::SKOLEM_NO_NOTIFY
);
3854 subs
.addSubstitution(func
, func2
);
3855 if(subs
.apply(n
) != n
) {
3856 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl
;
3858 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
3859 << "considering model value for " << func
<< endl
3860 << "body of lambda is: " << val
<< endl
;
3862 ss
<< "body substitutes to: " << n
<< endl
;
3864 ss
<< "so " << func
<< " is defined in terms of itself." << endl
3865 << "Run with `--check-models -v' for additional diagnostics.";
3866 InternalError(ss
.str());
3870 // (2) check that the value is actually a value
3871 else if (!val
.isConst()) {
3872 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl
;
3874 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
3875 << "model value for " << func
<< endl
3876 << " is " << val
<< endl
3877 << "and that is not a constant (.isConst() == false)." << endl
3878 << "Run with `--check-models -v' for additional diagnostics.";
3879 InternalError(ss
.str());
3882 // (3) check that it's the correct (sub)type
3883 // This was intended to be a more general check, but for now we can't do that because
3884 // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
3885 else if(func
.getType().isInteger() && !val
.getType().isInteger()) {
3886 Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl
;
3888 ss
<< "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
3889 << "model value for " << func
<< endl
3890 << " is " << val
<< endl
3891 << "value type is " << val
.getType() << endl
3892 << "should be of type " << func
.getType() << endl
3893 << "Run with `--check-models -v' for additional diagnostics.";
3894 InternalError(ss
.str());
3897 // (4) checks complete, add the substitution
3898 Debug("boolean-terms") << "cm: adding subs " << func
<< " :=> " << val
<< endl
;
3899 substitutions
.addSubstitution(func
, val
);
3903 // Now go through all our user assertions checking if they're satisfied.
3904 for(AssertionList::const_iterator i
= d_assertionList
->begin(); i
!= d_assertionList
->end(); ++i
) {
3905 Notice() << "SmtEngine::checkModel(): checking assertion " << *i
<< endl
;
3906 Node n
= Node::fromExpr(*i
);
3908 // Apply any define-funs from the problem.
3910 hash_map
<Node
, Node
, NodeHashFunction
> cache
;
3911 n
= d_private
->expandDefinitions(n
, cache
);
3913 Notice() << "SmtEngine::checkModel(): -- expands to " << n
<< endl
;
3915 // Apply our model value substitutions.
3916 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
3917 n
= substitutions
.apply(n
);
3918 Debug("boolean-terms") << "++ got " << n
<< endl
;
3919 Notice() << "SmtEngine::checkModel(): -- substitutes to " << n
<< endl
;
3921 //AJR : FIXME need to ignore quantifiers too?
3922 if( n
.getKind() != kind::REWRITE_RULE
){
3923 // In case it's a quantifier (or contains one), look up its value before
3924 // simplifying, or the quantifier might be irreparably altered.
3927 // Note this "skip" is done here, rather than above. This is
3928 // because (1) the quantifier could in principle simplify to false,
3929 // which should be reported, and (2) checking for the quantifier
3930 // above, before simplification, doesn't catch buried quantifiers
3931 // anyway (those not at the top-level).
3932 Notice() << "SmtEngine::checkModel(): -- skipping quantifiers/rewrite-rules assertion"
3937 // Simplify the result.
3938 n
= d_private
->simplify(n
);
3939 Notice() << "SmtEngine::checkModel(): -- simplifies to " << n
<< endl
;
3941 // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
3942 n
= d_private
->d_iteRemover
.replace(n
);
3943 Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n
<< endl
;
3945 // Apply our model value substitutions (again), as things may have been simplified.
3946 Debug("boolean-terms") << "applying subses to " << n
<< endl
;
3947 n
= substitutions
.apply(n
);
3948 Debug("boolean-terms") << "++ got " << n
<< endl
;
3949 Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n
<< endl
;
3951 // As a last-ditch effort, ask model to simplify it.
3952 // Presently, this is only an issue for quantifiers, which can have a value
3953 // but don't show up in our substitution map above.
3955 Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n
<< endl
;
3956 AlwaysAssert(!hardFailure
|| n
.isConst() || n
.getKind() == kind::LAMBDA
);
3958 // The result should be == true.
3959 if(n
!= NodeManager::currentNM()->mkConst(true)) {
3960 Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
3963 ss
<< "SmtEngine::checkModel(): "
3964 << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
3965 << "assertion: " << *i
<< endl
3966 << "simplifies to: " << n
<< endl
3967 << "expected `true'." << endl
3968 << "Run with `--check-models -v' for additional diagnostics.";
3970 InternalError(ss
.str());
3972 Warning() << ss
.str() << endl
;
3976 Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl
;
3979 UnsatCore
SmtEngine::getUnsatCore() throw(ModalException
) {
3980 Trace("smt") << "SMT getUnsatCore()" << endl
;
3981 SmtScope
smts(this);
3982 finalOptionsAreSet();
3983 if(Dump
.isOn("benchmark")) {
3984 Dump("benchmark") << GetUnsatCoreCommand();
3987 if(!options::unsatCores()) {
3988 throw ModalException("Cannot get an unsat core when produce-unsat-cores option is off.");
3990 if(d_status
.isNull() ||
3991 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
3992 d_problemExtended
) {
3993 throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.");
3996 d_proofManager
->getProof(this);// just to trigger core creation
3997 return UnsatCore(this, d_proofManager
->begin_unsat_core(), d_proofManager
->end_unsat_core());
3998 #else /* CVC4_PROOF */
3999 throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");
4000 #endif /* CVC4_PROOF */
4003 Proof
* SmtEngine::getProof() throw(ModalException
) {
4004 Trace("smt") << "SMT getProof()" << endl
;
4005 SmtScope
smts(this);
4006 finalOptionsAreSet();
4007 if(Dump
.isOn("benchmark")) {
4008 Dump("benchmark") << GetProofCommand();
4011 if(!options::proof()) {
4012 throw ModalException("Cannot get a proof when produce-proofs option is off.");
4014 if(d_status
.isNull() ||
4015 d_status
.asSatisfiabilityResult() != Result::UNSAT
||
4016 d_problemExtended
) {
4017 throw ModalException("Cannot get a proof unless immediately preceded by UNSAT/VALID response.");
4020 return ProofManager::getProof(this);
4021 #else /* CVC4_PROOF */
4022 throw ModalException("This build of CVC4 doesn't have proof support.");
4023 #endif /* CVC4_PROOF */
4026 void SmtEngine::printInstantiations( std::ostream
& out
) {
4027 SmtScope
smts(this);
4028 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
4029 out
<< "% SZS output start Proof for " << d_filename
.c_str() << std::endl
;
4031 if( d_theoryEngine
){
4032 d_theoryEngine
->printInstantiations( out
);
4034 if( options::instFormatMode()==INST_FORMAT_MODE_SZS
){
4035 out
<< "% SZS output end Proof for " << d_filename
.c_str() << std::endl
;
4039 vector
<Expr
> SmtEngine::getAssertions() throw(ModalException
) {
4040 SmtScope
smts(this);
4041 finalOptionsAreSet();
4042 if(Dump
.isOn("benchmark")) {
4043 Dump("benchmark") << GetAssertionsCommand();
4045 Trace("smt") << "SMT getAssertions()" << endl
;
4046 if(!options::interactive()) {
4048 "Cannot query the current assertion list when not in interactive mode.";
4049 throw ModalException(msg
);
4051 Assert(d_assertionList
!= NULL
);
4052 // copy the result out
4053 return vector
<Expr
>(d_assertionList
->begin(), d_assertionList
->end());
4056 void SmtEngine::push() throw(ModalException
, LogicException
) {
4057 SmtScope
smts(this);
4058 finalOptionsAreSet();
4060 Trace("smt") << "SMT push()" << endl
;
4061 d_private
->processAssertions();
4062 if(Dump
.isOn("benchmark")) {
4063 Dump("benchmark") << PushCommand();
4065 if(!options::incrementalSolving()) {
4066 throw ModalException("Cannot push when not solving incrementally (use --incremental)");
4069 // check to see if a postsolve() is pending
4070 if(d_needPostsolve
) {
4071 d_theoryEngine
->postsolve();
4072 d_needPostsolve
= false;
4075 // The problem isn't really "extended" yet, but this disallows
4076 // get-model after a push, simplifying our lives somewhat and
4077 // staying symmtric with pop.
4078 d_problemExtended
= true;
4080 d_userLevels
.push_back(d_userContext
->getLevel());
4082 Trace("userpushpop") << "SmtEngine: pushed to level "
4083 << d_userContext
->getLevel() << endl
;
4086 void SmtEngine::pop() throw(ModalException
) {
4087 SmtScope
smts(this);
4088 finalOptionsAreSet();
4089 Trace("smt") << "SMT pop()" << endl
;
4090 if(Dump
.isOn("benchmark")) {
4091 Dump("benchmark") << PopCommand();
4093 if(!options::incrementalSolving()) {
4094 throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
4096 if(d_userLevels
.size() == 0) {
4097 throw ModalException("Cannot pop beyond the first user frame");
4100 // check to see if a postsolve() is pending
4101 if(d_needPostsolve
) {
4102 d_theoryEngine
->postsolve();
4103 d_needPostsolve
= false;
4106 // The problem isn't really "extended" yet, but this disallows
4107 // get-model after a pop, simplifying our lives somewhat. It might
4108 // not be strictly necessary to do so, since the pops occur lazily,
4109 // but also it would be weird to have a legally-executed (get-model)
4110 // that only returns a subset of the assignment (because the rest
4111 // is no longer in scope!).
4112 d_problemExtended
= true;
4114 AlwaysAssert(d_userContext
->getLevel() > 0);
4115 AlwaysAssert(d_userLevels
.back() < d_userContext
->getLevel());
4116 while (d_userLevels
.back() < d_userContext
->getLevel()) {
4119 d_userLevels
.pop_back();
4121 // Clear out assertion queues etc., in case anything is still in there
4122 d_private
->notifyPop();
4124 Trace("userpushpop") << "SmtEngine: popped to level "
4125 << d_userContext
->getLevel() << endl
;
4126 // FIXME: should we reset d_status here?
4127 // SMT-LIBv2 spec seems to imply no, but it would make sense to..
4128 // Still, we want the right exit status after any final sequence
4132 void SmtEngine::internalPush() {
4133 Assert(d_fullyInited
);
4134 Trace("smt") << "SmtEngine::internalPush()" << endl
;
4136 if(options::incrementalSolving()) {
4137 d_private
->processAssertions();
4138 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
4139 d_userContext
->push();
4140 // the d_context push is done inside of the SAT solver
4141 d_propEngine
->push();
4145 void SmtEngine::internalPop(bool immediate
) {
4146 Assert(d_fullyInited
);
4147 Trace("smt") << "SmtEngine::internalPop()" << endl
;
4148 if(options::incrementalSolving()) {
4156 void SmtEngine::doPendingPops() {
4157 Assert(d_pendingPops
== 0 || options::incrementalSolving());
4158 while(d_pendingPops
> 0) {
4159 TimerStat::CodeTimer
pushPopTimer(d_stats
->d_pushPopTime
);
4160 d_propEngine
->pop();
4161 // the d_context pop is done inside of the SAT solver
4162 d_userContext
->pop();
4167 void SmtEngine::interrupt() throw(ModalException
) {
4168 if(!d_fullyInited
) {
4171 d_propEngine
->interrupt();
4172 d_theoryEngine
->interrupt();
4175 void SmtEngine::setResourceLimit(unsigned long units
, bool cumulative
) {
4177 Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units
<< endl
;
4178 d_resourceBudgetCumulative
= (units
== 0) ? 0 : (d_cumulativeResourceUsed
+ units
);
4180 Trace("limit") << "SmtEngine: setting per-call resource limit to " << units
<< endl
;
4181 d_resourceBudgetPerCall
= units
;
4185 void SmtEngine::setTimeLimit(unsigned long millis
, bool cumulative
) {
4187 Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis
<< " ms" << endl
;
4188 d_timeBudgetCumulative
= (millis
== 0) ? 0 : (d_cumulativeTimeUsed
+ millis
);
4190 Trace("limit") << "SmtEngine: setting per-call time limit to " << millis
<< " ms" << endl
;
4191 d_timeBudgetPerCall
= millis
;
4195 unsigned long SmtEngine::getResourceUsage() const {
4196 return d_cumulativeResourceUsed
;
4199 unsigned long SmtEngine::getTimeUsage() const {
4200 return d_cumulativeTimeUsed
;
4203 unsigned long SmtEngine::getResourceRemaining() const throw(ModalException
) {
4204 if(d_resourceBudgetCumulative
== 0) {
4205 throw ModalException("No cumulative resource limit is currently set");
4208 return d_resourceBudgetCumulative
<= d_cumulativeResourceUsed
? 0 :
4209 d_resourceBudgetCumulative
- d_cumulativeResourceUsed
;
4212 unsigned long SmtEngine::getTimeRemaining() const throw(ModalException
) {
4213 if(d_timeBudgetCumulative
== 0) {
4214 throw ModalException("No cumulative time limit is currently set");
4217 return d_timeBudgetCumulative
<= d_cumulativeTimeUsed
? 0 :
4218 d_timeBudgetCumulative
- d_cumulativeTimeUsed
;
4221 Statistics
SmtEngine::getStatistics() const throw() {
4222 return Statistics(*d_statisticsRegistry
);
4225 SExpr
SmtEngine::getStatistic(std::string name
) const throw() {
4226 return d_statisticsRegistry
->getStatistic(name
);
4229 void SmtEngine::setUserAttribute(const std::string
& attr
, Expr expr
, std::vector
<Expr
> expr_values
, std::string str_value
) {
4230 SmtScope
smts(this);
4231 std::vector
<Node
> node_values
;
4232 for( unsigned i
=0; i
<expr_values
.size(); i
++ ){
4233 node_values
.push_back( expr_values
[i
].getNode() );
4235 d_theoryEngine
->setUserAttribute(attr
, expr
.getNode(), node_values
, str_value
);
4238 void SmtEngine::setPrintFuncInModel(Expr f
, bool p
) {
4239 Trace("setp-model") << "Set printInModel " << f
<< " to " << p
<< std::endl
;
4240 for( unsigned i
=0; i
<d_modelGlobalCommands
.size(); i
++ ){
4241 Command
* c
= d_modelGlobalCommands
[i
];
4242 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
4244 if( dfc
->getFunction()==f
){
4245 dfc
->setPrintInModel( p
);
4249 for( unsigned i
=0; i
<d_modelCommands
->size(); i
++ ){
4250 Command
* c
= (*d_modelCommands
)[i
];
4251 DeclareFunctionCommand
* dfc
= dynamic_cast<DeclareFunctionCommand
*>(c
);
4253 if( dfc
->getFunction()==f
){
4254 dfc
->setPrintInModel( p
);
4260 }/* CVC4 namespace */