1 

/********************* */ 
2 

/*! \file smt_engine.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Morgan Deters, Aina Niemetz 
6 

** This file is part of the CVC4 project. 
7 

** Copyright (c) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief SmtEngine: the main public entry point of libcvc4. 
13 

** 
14 

** SmtEngine: the main public entry point of libcvc4. 
15 

**/ 
16 


17 

#include "cvc4_public.h" 
18 


19 

#ifndef CVC4__SMT_ENGINE_H 
20 

#define CVC4__SMT_ENGINE_H 
21 


22 

#include <map> 
23 

#include <memory> 
24 

#include <string> 
25 

#include <vector> 
26 


27 

#include "context/cdhashmap_forward.h" 
28 

#include "cvc4_export.h" 
29 

#include "options/options.h" 
30 

#include "smt/output_manager.h" 
31 

#include "smt/smt_mode.h" 
32 

#include "theory/logic_info.h" 
33 

#include "util/result.h" 
34 

#include "util/sexpr.h" 
35 

#include "util/statistics.h" 
36 


37 

namespace CVC4 { 
38 


39 

template <bool ref_count> class NodeTemplate; 
40 

typedef NodeTemplate<true> Node; 
41 

typedef NodeTemplate<false> TNode; 
42 

class TypeNode; 
43 

struct NodeHashFunction; 
44 


45 

class Env; 
46 

class NodeManager; 
47 

class TheoryEngine; 
48 

class ProofManager; 
49 

class UnsatCore; 
50 

class LogicRequest; 
51 

class StatisticsRegistry; 
52 

class Printer; 
53 

class ResourceManager; 
54 


55 

/*  */ 
56 


57 

namespace api { 
58 

class Solver; 
59 

} // namespace api 
60 


61 

/*  */ 
62 


63 

namespace context { 
64 

class Context; 
65 

class UserContext; 
66 

}/* CVC4::context namespace */ 
67 


68 

/*  */ 
69 


70 

namespace preprocessing { 
71 

class PreprocessingPassContext; 
72 

} 
73 


74 

/*  */ 
75 


76 

namespace prop { 
77 

class PropEngine; 
78 

}/* CVC4::prop namespace */ 
79 


80 

/*  */ 
81 


82 

namespace smt { 
83 

/** Utilities */ 
84 

class Model; 
85 

class SmtEngineState; 
86 

class AbstractValues; 
87 

class Assertions; 
88 

class DumpManager; 
89 

class ResourceOutListener; 
90 

class SmtNodeManagerListener; 
91 

class OptionsManager; 
92 

class Preprocessor; 
93 

class CheckModels; 
94 

/** Subsolvers */ 
95 

class SmtSolver; 
96 

class SygusSolver; 
97 

class AbductionSolver; 
98 

class InterpolationSolver; 
99 

class QuantElimSolver; 
100 

/** 
101 

* Representation of a defined function. We keep these around in 
102 

* SmtEngine to permit expanding definitions late (and lazily), to 
103 

* support getValue() over defined functions, to support user output 
104 

* in terms of defined functions, etc. 
105 

*/ 
106 

class DefinedFunction; 
107 


108 

struct SmtEngineStatistics; 
109 

class SmtScope; 
110 

class PfManager; 
111 

class UnsatCoreManager; 
112 


113 

ProofManager* currentProofManager(); 
114 

}/* CVC4::smt namespace */ 
115 


116 

/*  */ 
117 


118 

namespace theory { 
119 

class Rewriter; 
120 

class QuantifiersEngine; 
121 

}/* CVC4::theory namespace */ 
122 


123 


124 

/*  */ 
125 


126 

class CVC4_EXPORT SmtEngine 
127 

{ 
128 

friend class ::CVC4::api::Solver; 
129 

friend class ::CVC4::smt::SmtEngineState; 
130 

friend class ::CVC4::smt::SmtScope; 
131 

friend class ::CVC4::LogicRequest; 
132 


133 

/* ....................................................................... */ 
134 

public: 
135 

/* ....................................................................... */ 
136 


137 

/** 
138 

* Construct an SmtEngine with the given expression manager. 
139 

* If provided, optr is a pointer to a set of options that should initialize the values 
140 

* of the options object owned by this class. 
141 

*/ 
142 

SmtEngine(NodeManager* nm, Options* optr = nullptr); 
143 

/** Destruct the SMT engine. */ 
144 

~SmtEngine(); 
145 


146 

// concerning the state 
147 


148 

/** 
149 

* This is the main initialization procedure of the SmtEngine. 
150 

* 
151 

* Should be called whenever the final options and logic for the problem are 
152 

* set (at least, those options that are not permitted to change after 
153 

* assertions and queries are made). 
154 

* 
155 

* Internally, this creates the theory engine, prop engine, decision engine, 
156 

* and other utilities whose initialization depends on the final set of 
157 

* options being set. 
158 

* 
159 

* This postconstruction initialization is automatically triggered by the 
160 

* use of the SmtEngine; e.g. when the first formula is asserted, a call 
161 

* to simplify() is issued, a scope is pushed, etc. 
162 

*/ 
163 

void finishInit(); 
164 

/** 
165 

* Return true if this SmtEngine is fully initialized (postconstruction) 
166 

* by the above call. 
167 

*/ 
168 

bool isFullyInited() const; 
169 

/** 
170 

* Return true if a checkEntailed() or checkSatisfiability() has been made. 
171 

*/ 
172 

bool isQueryMade() const; 
173 

/** Return the user context level. */ 
174 

size_t getNumUserLevels() const; 
175 

/** Return the current mode of the solver. */ 
176 

SmtMode getSmtMode() const; 
177 

/** 
178 

* Whether the SmtMode allows for getvalue, getmodel, getassignment, etc. 
179 

* This is equivalent to: 
180 

* getSmtMode()==SmtMode::SAT  getSmtMode()==SmtMode::SAT_UNKNOWN 
181 

*/ 
182 

bool isSmtModeSat() const; 
183 

/** 
184 

* Returns the most recent result of checkSat/checkEntailed or 
185 

* (setinfo :status). 
186 

*/ 
187 

Result getStatusOfLastCommand() const; 
188 

// end concerning the state 
189 


190 

/** 
191 

* Set the logic of the script. 
192 

* @throw ModalException, LogicException 
193 

*/ 
194 

void setLogic(const std::string& logic); 
195 


196 

/** 
197 

* Set the logic of the script. 
198 

* @throw ModalException, LogicException 
199 

*/ 
200 

void setLogic(const char* logic); 
201 


202 

/** 
203 

* Set the logic of the script. 
204 

* @throw ModalException 
205 

*/ 
206 

void setLogic(const LogicInfo& logic); 
207 


208 

/** Get the logic information currently set. */ 
209 

const LogicInfo& getLogicInfo() const; 
210 


211 

/** Get the logic information set by the user. */ 
212 

LogicInfo getUserLogicInfo() const; 
213 


214 

/** 
215 

* Set information about the script executing. 
216 

*/ 
217 

void setInfo(const std::string& key, const std::string& value); 
218 


219 

/** Return true if given keyword is a valid SMTLIB v2 getinfo flag. */ 
220 

bool isValidGetInfoFlag(const std::string& key) const; 
221 


222 

/** Query information about the SMT environment. */ 
223 

CVC4::SExpr getInfo(const std::string& key) const; 
224 


225 

/** 
226 

* Set an aspect of the current SMT execution environment. 
227 

* @throw OptionException, ModalException 
228 

*/ 
229 

void setOption(const std::string& key, const std::string& value); 
230 


231 

/** Set is internal subsolver. 
232 

* 
233 

* This function is called on SmtEngine objects that are created internally. 
234 

* It is used to mark that this SmtEngine should not perform preprocessing 
235 

* passes that rephrase the input, such as sygusrrsynthinput or 
236 

* sygusabduct. 
237 

*/ 
238 

void setIsInternalSubsolver(); 
239 

/** Is this an internal subsolver? */ 
240 

bool isInternalSubsolver() const; 
241 


242 

/** 
243 

* Notify that we are now parsing the input with the given filename. 
244 

* This call sets the filename maintained by this SmtEngine for bookkeeping 
245 

* and also makes a copy of the current options of this SmtEngine. This 
246 

* is required so that the SMTLIB command (reset) returns the SmtEngine 
247 

* to a state where its options were prior to parsing but after e.g. 
248 

* reading command line options. 
249 

*/ 
250 

void notifyStartParsing(const std::string& filename) CVC4_EXPORT; 
251 

/** return the input name (if any) */ 
252 

const std::string& getFilename() const; 
253 


254 

/** 
255 

* Helper method for the API to put the last check result into the statistics. 
256 

*/ 
257 

void setResultStatistic(const std::string& result) CVC4_EXPORT; 
258 

/** 
259 

* Helper method for the API to put the total runtime into the statistics. 
260 

*/ 
261 

void setTotalTimeStatistic(double seconds) CVC4_EXPORT; 
262 


263 

/** 
264 

* Get the model (only if immediately preceded by a SAT or NOT_ENTAILED 
265 

* query). Only permitted if producemodels is on. 
266 

*/ 
267 

smt::Model* getModel(); 
268 


269 

/** 
270 

* Block the current model. Can be called only if immediately preceded by 
271 

* a SAT or INVALID query. Only permitted if producemodels is on, and the 
272 

* blockmodels option is set to a mode other than "none". 
273 

* 
274 

* This adds an assertion to the assertion stack that blocks the current 
275 

* model based on the current options configured by CVC4. 
276 

* 
277 

* The return value has the same meaning as that of assertFormula. 
278 

*/ 
279 

Result blockModel(); 
280 


281 

/** 
282 

* Block the current model values of (at least) the values in exprs. 
283 

* Can be called only if immediately preceded by a SAT or NOT_ENTAILED query. 
284 

* Only permitted if producemodels is on, and the blockmodels option is set 
285 

* to a mode other than "none". 
286 

* 
287 

* This adds an assertion to the assertion stack of the form: 
288 

* (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn))) 
289 

* where M0 ... Mn are the current model values of exprs[0] ... exprs[n]. 
290 

* 
291 

* The return value has the same meaning as that of assertFormula. 
292 

*/ 
293 

Result blockModelValues(const std::vector<Node>& exprs); 
294 


295 

/** 
296 

* Declare heap. For smt2 inputs, this is called when the command 
297 

* (declareheap (locT datat)) is invoked by the user. This sets locT as the 
298 

* location type and dataT is the data type for the heap. This command should 
299 

* be executed only once, and must be invoked before solving separation logic 
300 

* inputs. 
301 

*/ 
302 

void declareSepHeap(TypeNode locT, TypeNode dataT); 
303 


304 

/** 
305 

* Get the separation heap types, which extracts which types were passed to 
306 

* the method above. 
307 

* 
308 

* @return true if the separation logic heap types have been declared. 
309 

*/ 
310 

bool getSepHeapTypes(TypeNode& locT, TypeNode& dataT); 
311 


312 

/** When using separation logic, obtain the expression for the heap. */ 
313 

Node getSepHeapExpr(); 
314 


315 

/** When using separation logic, obtain the expression for nil. */ 
316 

Node getSepNilExpr(); 
317 


318 

/** 
319 

* Get an aspect of the current SMT execution environment. 
320 

* @throw OptionException 
321 

*/ 
322 

Node getOption(const std::string& key) const; 
323 


324 

/** 
325 

* Define function func in the current context to be: 
326 

* (lambda (formals) formula) 
327 

* This adds func to the list of defined functions, which indicates that 
328 

* all occurrences of func should be expanded during expandDefinitions. 
329 

* 
330 

* @param func a variable of function type that expects the arguments in 
331 

* formal 
332 

* @param formals a list of BOUND_VARIABLE expressions 
333 

* @param formula The body of the function, must not contain func 
334 

* @param global True if this definition is global (i.e. should persist when 
335 

* popping the user context) 
336 

*/ 
337 

void defineFunction(Node func, 
338 

const std::vector<Node>& formals, 
339 

Node formula, 
340 

bool global = false); 
341 


342 

/** Return true if given expression is a defined function. */ 
343 

bool isDefinedFunction(Node func); 
344 


345 

/** 
346 

* Define functions recursive 
347 

* 
348 

* For each i, this constrains funcs[i] in the current context to be: 
349 

* (lambda (formals[i]) formulas[i]) 
350 

* where formulas[i] may contain variables from funcs. Unlike defineFunction 
351 

* above, we do not add funcs[i] to the set of defined functions. Instead, 
352 

* we consider funcs[i] to be a free uninterpreted function, and add: 
353 

* forall formals[i]. f(formals[i]) = formulas[i] 
354 

* to the set of assertions in the current context. 
355 

* This method expects input such that for each i: 
356 

*  func[i] : a variable of function type that expects the arguments in 
357 

* formals[i], and 
358 

*  formals[i] : a list of BOUND_VARIABLE expressions. 
359 

* 
360 

* @param global True if this definition is global (i.e. should persist when 
361 

* popping the user context) 
362 

*/ 
363 

void defineFunctionsRec(const std::vector<Node>& funcs, 
364 

const std::vector<std::vector<Node>>& formals, 
365 

const std::vector<Node>& formulas, 
366 

bool global = false); 
367 

/** 
368 

* Define function recursive 
369 

* Same as above, but for a single function. 
370 

*/ 
371 

void defineFunctionRec(Node func, 
372 

const std::vector<Node>& formals, 
373 

Node formula, 
374 

bool global = false); 
375 

/** 
376 

* Add a formula to the current context: preprocess, do pertheory 
377 

* setup, use processAssertionList(), asserting to Tsolver for 
378 

* literals and conjunction of literals. Returns false if 
379 

* immediately determined to be inconsistent. This version 
380 

* takes a Boolean flag to determine whether to include this asserted 
381 

* formula in an unsat core (if one is later requested). 
382 

* 
383 

* @throw TypeCheckingException, LogicException, UnsafeInterruptException 
384 

*/ 
385 

Result assertFormula(const Node& formula, bool inUnsatCore = true); 
386 


387 

/** 
388 

* Check if a given (set of) expression(s) is entailed with respect to the 
389 

* current set of assertions. We check this by asserting the negation of 
390 

* the (big AND over the) given (set of) expression(s). 
391 

* Returns ENTAILED, NOT_ENTAILED, or ENTAILMENT_UNKNOWN result. 
392 

* 
393 

* @throw Exception 
394 

*/ 
395 

Result checkEntailed(const Node& assumption, bool inUnsatCore = true); 
396 

Result checkEntailed(const std::vector<Node>& assumptions, 
397 

bool inUnsatCore = true); 
398 


399 

/** 
400 

* Assert a formula (if provided) to the current context and call 
401 

* check(). Returns SAT, UNSAT, or SAT_UNKNOWN result. 
402 

* 
403 

* @throw Exception 
404 

*/ 
405 

Result checkSat(); 
406 

Result checkSat(const Node& assumption, bool inUnsatCore = true); 
407 

Result checkSat(const std::vector<Node>& assumptions, 
408 

bool inUnsatCore = true); 
409 


410 

/** 
411 

* Returns a set of socalled "failed" assumptions. 
412 

* 
413 

* The returned set is a subset of the set of assumptions of a previous 
414 

* (unsatisfiable) call to checkSatisfiability. Calling checkSatisfiability 
415 

* with this set of failed assumptions still produces an unsat answer. 
416 

* 
417 

* Note that the returned set of failed assumptions is not necessarily 
418 

* minimal. 
419 

*/ 
420 

std::vector<Node> getUnsatAssumptions(void); 
421 


422 

/* sygus commands */ 
423 


424 

/** 
425 

* Add sygus variable declaration. 
426 

* 
427 

* Declared SyGuS variables may be used in SyGuS constraints, in which they 
428 

* are assumed to be universally quantified. 
429 

* 
430 

* In SyGuS semantics, declared functions are treated in the same manner as 
431 

* declared variables, i.e. as universally quantified (function) variables 
432 

* which can occur in the SyGuS constraints that compose the conjecture to 
433 

* which a function is being synthesized. Thus declared functions should use 
434 

* this method as well. 
435 

*/ 
436 

void declareSygusVar(Node var); 
437 


438 

/** 
439 

* Add a functiontosynthesize declaration. 
440 

* 
441 

* The given sygusType may not correspond to the actual function type of func 
442 

* but to a datatype encoding the syntax restrictions for the 
443 

* functiontosynthesize. In this case this information is stored to be used 
444 

* during solving. 
445 

* 
446 

* vars contains the arguments of the functiontosynthesize. These variables 
447 

* are also stored to be used during solving. 
448 

* 
449 

* isInv determines whether the functiontosynthesize is actually an 
450 

* invariant. This information is necessary if we are dumping a command 
451 

* corresponding to this declaration, so that it can be properly printed. 
452 

*/ 
453 

void declareSynthFun(Node func, 
454 

TypeNode sygusType, 
455 

bool isInv, 
456 

const std::vector<Node>& vars); 
457 

/** 
458 

* Same as above, without a sygus type. 
459 

*/ 
460 

void declareSynthFun(Node func, bool isInv, const std::vector<Node>& vars); 
461 


462 

/** Add a regular sygus constraint.*/ 
463 

void assertSygusConstraint(Node constraint); 
464 


465 

/** 
466 

* Add an invariant constraint. 
467 

* 
468 

* Invariant constraints are not explicitly declared: they are given in terms 
469 

* of the invarianttosynthesize, the pre condition, transition relation and 
470 

* post condition. The actual constraint is built based on the inputs of these 
471 

* place holder predicates : 
472 

* 
473 

* PRE(x) > INV(x) 
474 

* INV() ^ TRANS(x, x') > INV(x') 
475 

* INV(x) > POST(x) 
476 

* 
477 

* The regular and primed variables are retrieved from the declaration of the 
478 

* invarianttosynthesize. 
479 

*/ 
480 

void assertSygusInvConstraint(Node inv, Node pre, Node trans, Node post); 
481 

/** 
482 

* Assert a synthesis conjecture to the current context and call 
483 

* check(). Returns sat, unsat, or unknown result. 
484 

* 
485 

* The actual synthesis conjecture is built based on the previously 
486 

* communicated information to this module (universal variables, defined 
487 

* functions, functionstosynthesize, and which constraints compose it). The 
488 

* built conjecture is a higherorder formula of the form 
489 

* 
490 

* exists f1...fn . forall v1...vm . F 
491 

* 
492 

* in which f1...fn are the functionstosynthesize, v1...vm are the declared 
493 

* universal variables and F is the set of declared constraints. 
494 

* 
495 

* @throw Exception 
496 

*/ 
497 

Result checkSynth(); 
498 


499 

/* end of sygus commands */ 
500 


501 

/** 
502 

* Simplify a formula without doing "much" work. Does not involve 
503 

* the SAT Engine in the simplification, but uses the current 
504 

* definitions, assertions, and the current partial model, if one 
505 

* has been constructed. It also involves theory normalization. 
506 

* 
507 

* @throw TypeCheckingException, LogicException, UnsafeInterruptException 
508 

* 
509 

* @todo (design) is this meant to give an equivalent or an 
510 

* equisatisfiable formula? 
511 

*/ 
512 

Node simplify(const Node& e); 
513 


514 

/** 
515 

* Expand the definitions in a term or formula. 
516 

* 
517 

* @param n The node to expand 
518 

* @param expandOnly if true, then the expandDefinitions function of 
519 

* TheoryEngine is not called on subterms of n. 
520 

* 
521 

* @throw TypeCheckingException, LogicException, UnsafeInterruptException 
522 

*/ 
523 

Node expandDefinitions(const Node& n, bool expandOnly = true); 
524 


525 

/** 
526 

* Get the assigned value of an expr (only if immediately preceded by a SAT 
527 

* or NOT_ENTAILED query). Only permitted if the SmtEngine is set to operate 
528 

* interactively and producemodels is on. 
529 

* 
530 

* @throw ModalException, TypeCheckingException, LogicException, 
531 

* UnsafeInterruptException 
532 

*/ 
533 

Node getValue(const Node& e) const; 
534 


535 

/** 
536 

* Same as getValue but for a vector of expressions 
537 

*/ 
538 

std::vector<Node> getValues(const std::vector<Node>& exprs); 
539 


540 

/** print instantiations 
541 

* 
542 

* Print all instantiations for all quantified formulas on out, 
543 

* returns true if at least one instantiation was printed. The type of output 
544 

* (list, num, etc.) is determined by printInstMode. 
545 

*/ 
546 

void printInstantiations(std::ostream& out); 
547 

/** 
548 

* Print the current proof. This method should be called after an UNSAT 
549 

* response. It gets the proof of false from the PropEngine and passes 
550 

* it to the ProofManager, which postprocesses the proof and prints it 
551 

* in the proper format. 
552 

*/ 
553 

void printProof(); 
554 

/** 
555 

* Print solution for synthesis conjectures found by counterexample guided 
556 

* instantiation module. 
557 

*/ 
558 

void printSynthSolution(std::ostream& out); 
559 


560 

/** 
561 

* Get synth solution. 
562 

* 
563 

* This method returns true if we are in a state immediately preceded by 
564 

* a successful call to checkSynth. 
565 

* 
566 

* This method adds entries to solMap that map functionstosynthesize with 
567 

* their solutions, for all active conjectures. This should be called 
568 

* immediately after the solver answers unsat for sygus input. 
569 

* 
570 

* Specifically, given a sygus conjecture of the form 
571 

* exists x1...xn. forall y1...yn. P( x1...xn, y1...yn ) 
572 

* where x1...xn are second order bound variables, we map each xi to 
573 

* lambda term in solMap such that 
574 

* forall y1...yn. P( solMap[x1]...solMap[xn], y1...yn ) 
575 

* is a valid formula. 
576 

*/ 
577 

bool getSynthSolutions(std::map<Node, Node>& solMap); 
578 


579 

/** 
580 

* Do quantifier elimination. 
581 

* 
582 

* This function takes as input a quantified formula q 
583 

* of the form: 
584 

* Q x1...xn. P( x1...xn, y1...yn ) 
585 

* where P( x1...xn, y1...yn ) is a quantifierfree 
586 

* formula in a logic that supports quantifier elimination. 
587 

* Currently, the only logics supported by quantifier 
588 

* elimination is LRA and LIA. 
589 

* 
590 

* This function returns a formula ret such that, given 
591 

* the current set of formulas A asserted to this SmtEngine : 
592 

* 
593 

* If doFull = true, then 
594 

*  ( A ^ q ) and ( A ^ ret ) are equivalent 
595 

*  ret is quantifierfree formula containing 
596 

* only free variables in y1...yn. 
597 

* 
598 

* If doFull = false, then 
599 

*  (A ^ q) => (A ^ ret) if Q is forall or 
600 

* (A ^ ret) => (A ^ q) if Q is exists, 
601 

*  ret is quantifierfree formula containing 
602 

* only free variables in y1...yn, 
603 

*  If Q is exists, let A^Q_n be the formula 
604 

* A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n 
605 

* where for each i=1,...n, formula ret^Q_i 
606 

* is the result of calling doQuantifierElimination 
607 

* for q with the set of assertions A^Q_{i1}. 
608 

* Similarly, if Q is forall, then let A^Q_n be 
609 

* A ^ ret^Q_1 ^ ... ^ ret^Q_n 
610 

* where ret^Q_i is the same as above. 
611 

* In either case, we have that ret^Q_j will 
612 

* eventually be true or false, for some finite j. 
613 

* 
614 

* The former feature is quantifier elimination, and 
615 

* is run on invocations of the smt2 extended command getqe. 
616 

* The latter feature is referred to as partial quantifier 
617 

* elimination, and is run on invocations of the smt2 
618 

* extended command getqedisjunct, which can be used 
619 

* for incrementally computing the result of a 
620 

* quantifier elimination. 
621 

* 
622 

* The argument strict is whether to output 
623 

* warnings, such as when an unexpected logic is used. 
624 

* 
625 

* throw@ Exception 
626 

*/ 
627 

Node getQuantifierElimination(Node q, bool doFull, bool strict = true); 
628 


629 

/** 
630 

* This method asks this SMT engine to find an interpolant with respect to 
631 

* the current assertion stack (call it A) and the conjecture (call it B). If 
632 

* this method returns true, then interpolant is set to a formula I such that 
633 

* A ^ ~I and I ^ ~B are both unsatisfiable. 
634 

* 
635 

* The argument grammarType is a sygus datatype type that encodes the syntax 
636 

* restrictions on the shapes of possible solutions. 
637 

* 
638 

* This method invokes a separate copy of the SMT engine for solving the 
639 

* corresponding sygus problem for generating such a solution. 
640 

*/ 
641 

bool getInterpol(const Node& conj, 
642 

const TypeNode& grammarType, 
643 

Node& interpol); 
644 


645 

/** Same as above, but without userprovided grammar restrictions */ 
646 

bool getInterpol(const Node& conj, Node& interpol); 
647 


648 

/** 
649 

* This method asks this SMT engine to find an abduct with respect to the 
650 

* current assertion stack (call it A) and the conjecture (call it B). 
651 

* If this method returns true, then abd is set to a formula C such that 
652 

* A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable. 
653 

* 
654 

* The argument grammarType is a sygus datatype type that encodes the syntax 
655 

* restrictions on the shape of possible solutions. 
656 

* 
657 

* This method invokes a separate copy of the SMT engine for solving the 
658 

* corresponding sygus problem for generating such a solution. 
659 

*/ 
660 

bool getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd); 
661 


662 

/** Same as above, but without userprovided grammar restrictions */ 
663 

bool getAbduct(const Node& conj, Node& abd); 
664 


665 

/** 
666 

* Get list of quantified formulas that were instantiated on the last call 
667 

* to checksat. 
668 

*/ 
669 

void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs); 
670 


671 

/** 
672 

* Get instantiation term vectors for quantified formula q. 
673 

* 
674 

* This method is similar to above, but in the example above, we return the 
675 

* (vectors of) terms t1, ..., tn instead. 
676 

* 
677 

* Notice that these are not guaranteed to come in the same order as the 
678 

* instantiation lemmas above. 
679 

*/ 
680 

void getInstantiationTermVectors(Node q, 
681 

std::vector<std::vector<Node>>& tvecs); 
682 

/** 
683 

* As above but only the instantiations that were relevant for the 
684 

* refutation. 
685 

*/ 
686 

void getRelevantInstantiationTermVectors( 
687 

std::map<Node, std::vector<std::vector<Node>>>& insts); 
688 

/** 
689 

* Get instantiation term vectors, which maps each instantiated quantified 
690 

* formula to the list of instantiations for that quantified formula. This 
691 

* list is minimized if proofs are enabled, and this call is immediately 
692 

* preceded by an UNSAT or ENTAILED query 
693 

*/ 
694 

void getInstantiationTermVectors( 
695 

std::map<Node, std::vector<std::vector<Node>>>& insts); 
696 


697 

/** 
698 

* Get an unsatisfiable core (only if immediately preceded by an UNSAT or 
699 

* ENTAILED query). Only permitted if CVC4 was built with unsatcore support 
700 

* and produceunsatcores is on. 
701 

*/ 
702 

UnsatCore getUnsatCore(); 
703 


704 

/** 
705 

* Get a refutation proof (only if immediately preceded by an UNSAT or 
706 

* ENTAILED query). Only permitted if CVC4 was built with proof support and 
707 

* the proof option is on. */ 
708 

std::string getProof(); 
709 


710 

/** 
711 

* Get the current set of assertions. Only permitted if the 
712 

* SmtEngine is set to operate interactively. 
713 

*/ 
714 

std::vector<Node> getAssertions(); 
715 


716 

/** 
717 

* Push a userlevel context. 
718 

* throw@ ModalException, LogicException, UnsafeInterruptException 
719 

*/ 
720 

void push(); 
721 


722 

/** 
723 

* Pop a userlevel context. Throws an exception if nothing to pop. 
724 

* @throw ModalException 
725 

*/ 
726 

void pop(); 
727 


728 

/** 
729 

* Completely reset the state of the solver, as though destroyed and 
730 

* recreated. The result is as if newly constructed (so it still 
731 

* retains the same options structure and NodeManager). 
732 

*/ 
733 

void reset(); 
734 


735 

/** Reset all assertions, global declarations, etc. */ 
736 

void resetAssertions(); 
737 


738 

/** 
739 

* Interrupt a running query. This can be called from another thread 
740 

* or from a signal handler. Throws a ModalException if the SmtEngine 
741 

* isn't currently in a query. 
742 

* 
743 

* @throw ModalException 
744 

*/ 
745 

void interrupt(); 
746 


747 

/** 
748 

* Set a resource limit for SmtEngine operations. This is like a time 
749 

* limit, but it's deterministic so that reproducible results can be 
750 

* obtained. Currently, it's based on the number of conflicts. 
751 

* However, please note that the definition may change between different 
752 

* versions of CVC4 (as may the number of conflicts required, anyway), 
753 

* and it might even be different between instances of the same version 
754 

* of CVC4 on different platforms. 
755 

* 
756 

* A cumulative and noncumulative (percall) resource limit can be 
757 

* set at the same time. A call to setResourceLimit() with 
758 

* cumulative==true replaces any cumulative resource limit currently 
759 

* in effect; a call with cumulative==false replaces any percall 
760 

* resource limit currently in effect. Time limits can be set in 
761 

* addition to resource limits; the SmtEngine obeys both. That means 
762 

* that up to four independent limits can control the SmtEngine 
763 

* at the same time. 
764 

* 
765 

* When an SmtEngine is first created, it has no time or resource 
766 

* limits. 
767 

* 
768 

* Currently, these limits only cause the SmtEngine to stop what its 
769 

* doing when the limit expires (or very shortly thereafter); no 
770 

* heuristics are altered by the limits or the threat of them expiring. 
771 

* We reserve the right to change this in the future. 
772 

* 
773 

* @param units the resource limit, or 0 for no limit 
774 

* @param cumulative whether this resource limit is to be a cumulative 
775 

* resource limit for all remaining calls into the SmtEngine (true), or 
776 

* whether it's a percall resource limit (false); the default is false 
777 

*/ 
778 

void setResourceLimit(unsigned long units, bool cumulative = false); 
779 


780 

/** 
781 

* Set a percall time limit for SmtEngine operations. 
782 

* 
783 

* A percall time limit can be set at the same time and replaces 
784 

* any percall time limit currently in effect. 
785 

* Resource limits (either percall or cumulative) can be set in 
786 

* addition to a time limit; the SmtEngine obeys all three of them. 
787 

* 
788 

* Note that the percall timer only ticks away when one of the 
789 

* SmtEngine's workhorse functions (things like assertFormula(), 
790 

* checkEntailed(), checkSat(), and simplify()) are running. 
791 

* Between calls, the timer is still. 
792 

* 
793 

* When an SmtEngine is first created, it has no time or resource 
794 

* limits. 
795 

* 
796 

* Currently, these limits only cause the SmtEngine to stop what its 
797 

* doing when the limit expires (or very shortly thereafter); no 
798 

* heuristics are altered by the limits or the threat of them expiring. 
799 

* We reserve the right to change this in the future. 
800 

* 
801 

* @param millis the time limit in milliseconds, or 0 for no limit 
802 

*/ 
803 

void setTimeLimit(unsigned long millis); 
804 


805 

/** 
806 

* Get the current resource usage count for this SmtEngine. This 
807 

* function can be used to ascertain reasonable values to pass as 
808 

* resource limits to setResourceLimit(). 
809 

*/ 
810 

unsigned long getResourceUsage() const; 
811 


812 

/** Get the current millisecond count for this SmtEngine. */ 
813 

unsigned long getTimeUsage() const; 
814 


815 

/** 
816 

* Get the remaining resources that can be consumed by this SmtEngine 
817 

* according to the currentlyset cumulative resource limit. If there 
818 

* is not a cumulative resource limit set, this function throws a 
819 

* ModalException. 
820 

* 
821 

* @throw ModalException 
822 

*/ 
823 

unsigned long getResourceRemaining() const; 
824 


825 

/** Permit access to the underlying NodeManager. */ 
826 

NodeManager* getNodeManager() const; 
827 


828 

/** Export statistics from this SmtEngine. */ 
829 

Statistics getStatistics() const; 
830 


831 

/** Get the value of one named statistic from this SmtEngine. */ 
832 

SExpr getStatistic(std::string name) const; 
833 


834 

/** Flush statistics from this SmtEngine and the NodeManager it uses. */ 
835 

void flushStatistics(std::ostream& out) const; 
836 


837 

/** 
838 

* Flush statistics from this SmtEngine and the NodeManager it uses. Safe to 
839 

* use in a signal handler. 
840 

*/ 
841 

void safeFlushStatistics(int fd) const; 
842 


843 

/** 
844 

* Set user attribute. 
845 

* This function is called when an attribute is set by a user. 
846 

* In SMTLIBv2 this is done via the syntax (! expr :attr) 
847 

*/ 
848 

void setUserAttribute(const std::string& attr, 
849 

Node expr, 
850 

const std::vector<Node>& expr_values, 
851 

const std::string& str_value); 
852 


853 

/** Get the options object (const and nonconst versions) */ 
854 

Options& getOptions(); 
855 

const Options& getOptions() const; 
856 


857 

/** Get a pointer to the UserContext owned by this SmtEngine. */ 
858 

context::UserContext* getUserContext(); 
859 


860 

/** Get a pointer to the Context owned by this SmtEngine. */ 
861 

context::Context* getContext(); 
862 


863 

/** Get a pointer to the TheoryEngine owned by this SmtEngine. */ 
864 

TheoryEngine* getTheoryEngine(); 
865 


866 

/** Get a pointer to the PropEngine owned by this SmtEngine. */ 
867 

prop::PropEngine* getPropEngine(); 
868 


869 

/** 
870 

* Get a pointer to the ProofManager owned by this SmtEngine. 
871 

* TODO (project #37): this is the old proof manager and will be deleted 
872 

*/ 
873 
10231104 
ProofManager* getProofManager() { return d_proofManager.get(); }; 
874 


875 

/** Get the resource manager of this SMT engine */ 
876 

ResourceManager* getResourceManager() const; 
877 


878 

/** Permit access to the underlying dump manager. */ 
879 

smt::DumpManager* getDumpManager(); 
880 


881 

/** Get the printer used by this SMT engine */ 
882 

const Printer& getPrinter() const; 
883 


884 

/** Get the output manager for this SMT engine */ 
885 

OutputManager& getOutputManager(); 
886 


887 

/** Get a pointer to the Rewriter owned by this SmtEngine. */ 
888 

theory::Rewriter* getRewriter(); 
889 


890 

/** The type of our internal map of defined functions */ 
891 

using DefinedFunctionMap = 
892 

context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>; 
893 


894 

/** Get the defined function map */ 
895 
1869170 
DefinedFunctionMap* getDefinedFunctionMap() { return d_definedFunctions; } 
896 

/** 
897 

* Get expanded assertions. 
898 

* 
899 

* Return the set of assertions, after expanding definitions. 
900 

*/ 
901 

std::vector<Node> getExpandedAssertions(); 
902 

/* ....................................................................... */ 
903 

private: 
904 

/* ....................................................................... */ 
905 


906 

// disallow copy/assignment 
907 

SmtEngine(const SmtEngine&) = delete; 
908 

SmtEngine& operator=(const SmtEngine&) = delete; 
909 


910 

/** Set solver instance that owns this SmtEngine. */ 
911 
6120 
void setSolver(api::Solver* solver) { d_solver = solver; } 
912 


913 

/** Get a pointer to the (new) PfManager owned by this SmtEngine. */ 
914 

smt::PfManager* getPfManager() { return d_pfManager.get(); }; 
915 


916 

/** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */ 
917 

StatisticsRegistry* getStatisticsRegistry(); 
918 


919 

/** 
920 

* Internal method to get an unsatisfiable core (only if immediately preceded 
921 

* by an UNSAT or ENTAILED query). Only permitted if CVC4 was built with 
922 

* unsatcore support and produceunsatcores is on. Does not dump the 
923 

* command. 
924 

*/ 
925 

UnsatCore getUnsatCoreInternal(); 
926 


927 

/** 
928 

* Check that a generated proof checks. This method is the same as printProof, 
929 

* but does not print the proof. Like that method, it should be called 
930 

* after an UNSAT response. It ensures that a wellformed proof of false 
931 

* can be constructed by the combination of the PropEngine and ProofManager. 
932 

*/ 
933 

void checkProof(); 
934 


935 

/** 
936 

* Check that an unsatisfiable core is indeed unsatisfiable. 
937 

*/ 
938 

void checkUnsatCore(); 
939 


940 

/** 
941 

* Check that a generated Model (via getModel()) actually satisfies 
942 

* all user assertions. 
943 

*/ 
944 

void checkModel(bool hardFailure = true); 
945 


946 

/** 
947 

* Check that a solution to an interpolation problem is indeed a solution. 
948 

* 
949 

* The check is made by determining that the assertions imply the solution of 
950 

* the interpolation problem (interpol), and the solution implies the goal 
951 

* (conj). If these criteria are not met, an internal error is thrown. 
952 

*/ 
953 

void checkInterpol(Node interpol, 
954 

const std::vector<Node>& easserts, 
955 

const Node& conj); 
956 


957 

/** 
958 

* This is called by the destructor, just before destroying the 
959 

* PropEngine, TheoryEngine, and DecisionEngine (in that order). It 
960 

* is important because there are destruction ordering issues 
961 

* between PropEngine and Theory. 
962 

*/ 
963 

void shutdown(); 
964 


965 

/** 
966 

* Quick check of consistency in current context: calls 
967 

* processAssertionList() then look for inconsistency (based only on 
968 

* that). 
969 

*/ 
970 

Result quickCheck(); 
971 


972 

/** 
973 

* Get the (SMTlevel) model pointer, if we are in SAT mode. Otherwise, 
974 

* return nullptr. 
975 

* 
976 

* This ensures that the underlying theory model of the SmtSolver maintained 
977 

* by this class is currently available, which means that CVC4 is producing 
978 

* models, and is in "SAT mode", otherwise a recoverable exception is thrown. 
979 

* 
980 

* @param c used for giving an error message to indicate the context 
981 

* this method was called. 
982 

*/ 
983 

smt::Model* getAvailableModel(const char* c) const; 
984 

/** 
985 

* Get available quantifiers engine, which throws a modal exception if it 
986 

* does not exist. This can happen if a quantifiersspecific call (e.g. 
987 

* getInstantiatedQuantifiedFormulas) is called in a nonquantified logic. 
988 

* 
989 

* @param c used for giving an error message to indicate the context 
990 

* this method was called. 
991 

*/ 
992 

theory::QuantifiersEngine* getAvailableQuantifiersEngine(const char* c) const; 
993 


994 

//  callbacks from the state 
995 

/** 
996 

* Notify push pre, which is called just before the user context of the state 
997 

* pushes. This processes all pending assertions. 
998 

*/ 
999 

void notifyPushPre(); 
1000 

/** 
1001 

* Notify push post, which is called just after the user context of the state 
1002 

* pushes. This performs a push on the underlying prop engine. 
1003 

*/ 
1004 

void notifyPushPost(); 
1005 

/** 
1006 

* Notify pop pre, which is called just before the user context of the state 
1007 

* pops. This performs a pop on the underlying prop engine. 
1008 

*/ 
1009 

void notifyPopPre(); 
1010 

/** 
1011 

* Notify post solve pre, which is called once per checksat query. It 
1012 

* is triggered when the first d_state.doPendingPops() is issued after the 
1013 

* checksat. This method is called before the contexts pop in the method 
1014 

* doPendingPops. 
1015 

*/ 
1016 

void notifyPostSolvePre(); 
1017 

/** 
1018 

* Same as above, but after contexts are popped. This calls the postsolve 
1019 

* method of the underlying TheoryEngine. 
1020 

*/ 
1021 

void notifyPostSolvePost(); 
1022 

//  end callbacks from the state 
1023 


1024 

/** 
1025 

* Internally handle the setting of a logic. This function should always 
1026 

* be called when d_logic is updated. 
1027 

*/ 
1028 

void setLogicInternal(); 
1029 


1030 

/* 
1031 

* Check satisfiability (used to check satisfiability and entailment). 
1032 

*/ 
1033 

Result checkSatInternal(const std::vector<Node>& assumptions, 
1034 

bool inUnsatCore, 
1035 

bool isEntailmentCheck); 
1036 


1037 

/** 
1038 

* Check that all Expr in formals are of BOUND_VARIABLE kind, where func is 
1039 

* the function that the formal argument list is for. This method is used 
1040 

* as a helper function when defining (recursive) functions. 
1041 

*/ 
1042 

void debugCheckFormals(const std::vector<Node>& formals, Node func); 
1043 


1044 

/** 
1045 

* Checks whether formula is a valid function body for func whose formal 
1046 

* argument list is stored in formals. This method is 
1047 

* used as a helper function when defining (recursive) functions. 
1048 

*/ 
1049 

void debugCheckFunctionBody(Node formula, 
1050 

const std::vector<Node>& formals, 
1051 

Node func); 
1052 


1053 

/** 
1054 

* Helper method to obtain both the heap and nil from the solver. Returns a 
1055 

* std::pair where the first element is the heap expression and the second 
1056 

* element is the nil expression. 
1057 

*/ 
1058 

std::pair<Node, Node> getSepHeapAndNilExpr(); 
1059 


1060 

/* Members  */ 
1061 


1062 

/** Solver instance that owns this SmtEngine instance. */ 
1063 

api::Solver* d_solver = nullptr; 
1064 


1065 

/** 
1066 

* The environment object, which contains all utilities that are globally 
1067 

* available to internal code. 
1068 

*/ 
1069 

std::unique_ptr<Env> d_env; 
1070 

/** 
1071 

* The state of this SmtEngine, which is responsible for maintaining which 
1072 

* SMT mode we are in, the contexts, the last result, etc. 
1073 

*/ 
1074 

std::unique_ptr<smt::SmtEngineState> d_state; 
1075 


1076 

/** Abstract values */ 
1077 

std::unique_ptr<smt::AbstractValues> d_absValues; 
1078 

/** Assertions manager */ 
1079 

std::unique_ptr<smt::Assertions> d_asserts; 
1080 

/** Resource out listener */ 
1081 

std::unique_ptr<smt::ResourceOutListener> d_routListener; 
1082 

/** Node manager listener */ 
1083 

std::unique_ptr<smt::SmtNodeManagerListener> d_snmListener; 
1084 


1085 

/** The SMT solver */ 
1086 

std::unique_ptr<smt::SmtSolver> d_smtSolver; 
1087 


1088 

/** The (old) proof manager TODO (project #37): delete this */ 
1089 

std::unique_ptr<ProofManager> d_proofManager; 
1090 

/** 
1091 

* The SMTlevel model object, which contains information about how to 
1092 

* print the model, as well as a pointer to the underlying TheoryModel 
1093 

* implementation maintained by the SmtSolver. 
1094 

*/ 
1095 

std::unique_ptr<smt::Model> d_model; 
1096 


1097 

/** 
1098 

* The utility used for checking models 
1099 

*/ 
1100 

std::unique_ptr<smt::CheckModels> d_checkModels; 
1101 


1102 

/** 
1103 

* The proof manager, which manages all things related to checking, 
1104 

* processing, and printing proofs. 
1105 

*/ 
1106 

std::unique_ptr<smt::PfManager> d_pfManager; 
1107 


1108 

/** 
1109 

* The unsat core manager, which produces unsat cores and related information 
1110 

* from refutations. */ 
1111 

std::unique_ptr<smt::UnsatCoreManager> d_ucManager; 
1112 


1113 

/** An index of our defined functions */ 
1114 

DefinedFunctionMap* d_definedFunctions; 
1115 


1116 

/** The solver for sygus queries */ 
1117 

std::unique_ptr<smt::SygusSolver> d_sygusSolver; 
1118 


1119 

/** The solver for abduction queries */ 
1120 

std::unique_ptr<smt::AbductionSolver> d_abductSolver; 
1121 

/** The solver for interpolation queries */ 
1122 

std::unique_ptr<smt::InterpolationSolver> d_interpolSolver; 
1123 

/** The solver for quantifier elimination queries */ 
1124 

std::unique_ptr<smt::QuantElimSolver> d_quantElimSolver; 
1125 


1126 

/** 
1127 

* The logic set by the user. The actual logic, which may extend the user's 
1128 

* logic, lives in the Env class. 
1129 

*/ 
1130 

LogicInfo d_userLogic; 
1131 


1132 

/** 
1133 

* Keep a copy of the original option settings (for reset()). The current 
1134 

* options live in the Env object. 
1135 

*/ 
1136 

Options d_originalOptions; 
1137 


1138 

/** Whether this is an internal subsolver. */ 
1139 

bool d_isInternalSubsolver; 
1140 


1141 

/** 
1142 

* Verbosity of various commands. 
1143 

*/ 
1144 

std::map<std::string, Integer> d_commandVerbosity; 
1145 


1146 

/** The statistics class */ 
1147 

std::unique_ptr<smt::SmtEngineStatistics> d_stats; 
1148 


1149 

/** the output manager for commands */ 
1150 

mutable OutputManager d_outMgr; 
1151 

/** 
1152 

* The options manager, which is responsible for implementing core options 
1153 

* such as those related to time outs and printing. It is also responsible 
1154 

* for set default options based on the logic. 
1155 

*/ 
1156 

std::unique_ptr<smt::OptionsManager> d_optm; 
1157 

/** 
1158 

* The preprocessor. 
1159 

*/ 
1160 

std::unique_ptr<smt::Preprocessor> d_pp; 
1161 

/** 
1162 

* The global scope object. Upon creation of this SmtEngine, it becomes the 
1163 

* SmtEngine in scope. It says the SmtEngine in scope until it is destructed, 
1164 

* or another SmtEngine is created. 
1165 

*/ 
1166 

std::unique_ptr<smt::SmtScope> d_scope; 
1167 

}; /* class SmtEngine */ 
1168 


1169 

/*  */ 
1170 


1171 

}/* CVC4 namespace */ 
1172 


1173 

#endif /* CVC4__SMT_ENGINE_H */ 