1 /********************* */
2 /*! \file abduction_solver.h
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief The solver for abduction queries
15 #include "cvc4_private.h"
17 #ifndef CVC4__SMT__ABDUCTION_SOLVER_H
18 #define CVC4__SMT__ABDUCTION_SOLVER_H
20 #include "expr/node.h"
21 #include "expr/type_node.h"
30 * A solver for abduction queries.
32 * This class is responsible for responding to get-abduct commands. It spawns
33 * a subsolver SmtEngine for a sygus conjecture that captures the abduction
34 * query, and implements supporting utility methods such as checkAbduct.
39 AbductionSolver(SmtEngine
* parent
);
42 * This method asks this SMT engine to find an abduct with respect to the
43 * current assertion stack (call it A) and the goal (call it B).
44 * If this method returns true, then abd is set to a formula C such that
45 * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable.
47 * @param goal The goal of the abduction problem.
48 * @param grammarType A sygus datatype type that encodes the syntax
49 * restrictions on the shape of possible solutions.
50 * @param abd This argument is updated to contain the solution to the
51 * abduction problem. Notice that this is a formula whose free symbols
52 * are contained in goal + the parent's current assertion stack.
54 * This method invokes a separate copy of the SMT engine for solving the
55 * corresponding sygus problem for generating such a solution.
57 bool getAbduct(const Node
& goal
, const TypeNode
& grammarType
, Node
& abd
);
60 * Same as above, but without user-provided grammar restrictions. A default
61 * grammar is chosen internally using the sygus grammar constructor utility.
63 bool getAbduct(const Node
& goal
, Node
& abd
);
66 * Check that a solution to an abduction conjecture is indeed a solution.
68 * The check is made by determining that the assertions conjoined with the
69 * solution to the abduction problem (a) is SAT, and the assertions conjoined
70 * with the abduct and the goal is UNSAT. If these criteria are not met, an
71 * internal error is thrown.
73 void checkAbduct(Node a
);
77 * Get abduct internal.
79 * Get the next abduct from the internal subsolver d_subsolver. If
80 * successful, this method returns true and sets abd to that abduct.
82 * This method assumes d_subsolver has been initialized to do abduction
85 bool getAbductInternal(Node
& abd
);
86 /** The parent SMT engine */
88 /** The SMT engine subsolver
90 * This is a separate copy of the SMT engine which is used for making
91 * calls that cannot be answered by this copy of the SMT engine. An example
92 * of invoking this subsolver is the get-abduct command, where we wish to
93 * solve a sygus conjecture based on the current assertions. In particular,
97 * In the copy of the SMT engine where these commands are issued, we maintain
98 * A in the assertion stack. To solve the abduction problem, instead of
99 * modifying the assertion stack to remove A and add the sygus conjecture
100 * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the
101 * assertion stack unchaged. This copy of the SMT engine can be further
102 * queried for information regarding further solutions.
104 std::unique_ptr
<SmtEngine
> d_subsolver
;
106 * The conjecture of the current abduction problem. This expression is only
107 * valid while the parent SmtEngine is in mode SMT_MODE_ABDUCT.
111 * If applicable, the function-to-synthesize that the subsolver is solving
112 * for. This is used for the get-abduct command.
120 #endif /* CVC4__SMT__ABDUCTION_SOLVER_H */