diff options
Diffstat (limited to 'src/prop/prop_engine.h')
| -rw-r--r-- | src/prop/prop_engine.h | 34 |
1 files changed, 10 insertions, 24 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 99c615211..773b27de4 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -111,34 +111,20 @@ class PropEngine theory::TrustNode removeItes(TNode node, std::vector<theory::TrustNode>& ppLemmas, std::vector<Node>& ppSkolems); - /** - * Notify preprocessed assertions. This method is called just before the - * assertions are asserted to this prop engine. This method notifies the - * theory engine of the given assertions. Notice this vector includes - * both the input formulas and the skolem definitions. - */ - void notifyPreprocessedAssertions(const std::vector<Node>& assertions); /** - * Converts the given formula to CNF and assert the CNF to the SAT solver. - * The formula is asserted permanently for the current context. Note the - * formula should correspond to an input formula and not a lemma introduced - * by term formula removal (which instead should use the interface below). - * @param node the formula to assert - */ - void assertFormula(TNode node); - /** - * Same as above, but node corresponds to the skolem definition of the given - * skolem. - * @param node the formula to assert - * @param skolem the skolem that this lemma defines. + * Converts the given formulas to CNF and assert the CNF to the SAT solver. + * These formulas are asserted permanently for the current context. + * Information about which assertions correspond to skolem definitions is + * contained in skolemMap. * - * For example, if k is introduced by ITE removal of (ite C x y), then node - * is the formula (ite C (= k x) (= k y)). It is important to distinguish - * these kinds of lemmas from input assertions, as the justification decision - * heuristic treates them specially. + * @param assertions the formulas to assert + * @param skolemMap a map which says which skolem (if any) each assertion + * corresponds to. For example, if (ite C (= k a) (= k b)) is the i^th + * assertion, then skolemMap may contain the entry { i -> k }. */ - void assertSkolemDefinition(TNode node, TNode skolem); + void assertInputFormulas(const std::vector<Node>& assertions, + std::unordered_map<size_t, Node>& skolemMap); /** * Converts the given formula to CNF and assert the CNF to the SAT solver. |