GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/smt_engine.h Lines: 3 3 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
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) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level 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 post-construction 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 (post-construction)
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 get-value, get-model, get-assignment, 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
   * (set-info :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 SMT-LIB v2 get-info 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 --sygus-rr-synth-input or
236
   * --sygus-abduct.
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 SMT-LIB 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 produce-models 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 produce-models is on, and the
272
   * block-models 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 produce-models is on, and the block-models 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
   * (declare-heap (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 per-theory
377
   * setup, use processAssertionList(), asserting to T-solver 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 so-called "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 function-to-synthesize 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
   * function-to-synthesize. In this case this information is stored to be used
444
   * during solving.
445
   *
446
   * vars contains the arguments of the function-to-synthesize. These variables
447
   * are also stored to be used during solving.
448
   *
449
   * isInv determines whether the function-to-synthesize 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 invariant-to-synthesize, 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
   * invariant-to-synthesize.
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, functions-to-synthesize, and which constraints compose it). The
488
   * built conjecture is a higher-order formula of the form
489
   *
490
   * exists f1...fn . forall v1...vm . F
491
   *
492
   * in which f1...fn are the functions-to-synthesize, 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 produce-models 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 post-processes the proof and prints it
551
   * in the proper format.
552
   */
553
  void printProof();
554
  /**
555
   * Print solution for synthesis conjectures found by counter-example 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 functions-to-synthesize 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 quantifier-free
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 quantifier-free 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 quantifier-free 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_{i-1}.
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 get-qe.
616
   * The latter feature is referred to as partial quantifier
617
   * elimination, and is run on invocations of the smt2
618
   * extended command get-qe-disjunct, 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 user-provided 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 user-provided 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 check-sat.
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 unsat-core support
700
   * and produce-unsat-cores 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 user-level context.
718
   * throw@ ModalException, LogicException, UnsafeInterruptException
719
   */
720
  void push();
721
722
  /**
723
   * Pop a user-level 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 non-cumulative (per-call) 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 per-call
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 per-call resource limit (false); the default is false
777
   */
778
  void setResourceLimit(unsigned long units, bool cumulative = false);
779
780
  /**
781
   * Set a per-call time limit for SmtEngine operations.
782
   *
783
   * A per-call time limit can be set at the same time and replaces
784
   * any per-call time limit currently in effect.
785
   * Resource limits (either per-call or cumulative) can be set in
786
   * addition to a time limit; the SmtEngine obeys all three of them.
787
   *
788
   * Note that the per-call 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 currently-set 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 SMT-LIBv2 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 non-const 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
   * unsat-core support and produce-unsat-cores 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 well-formed 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 (SMT-level) 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 quantifiers-specific call (e.g.
987
   * getInstantiatedQuantifiedFormulas) is called in a non-quantified 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 check-sat query. It
1012
   * is triggered when the first d_state.doPendingPops() is issued after the
1013
   * check-sat. 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 SMT-level 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 */