From c335e4d3fa8038bcff96d420b0d487641292c061 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 2 Feb 2022 20:25:14 -0800 Subject: [PATCH] Rename kind PLUS -> ADD. (#8036) This renames the arithmetic internal and API kind PLUS to ADD for consistency with our naming scheme for other operators (e.g., BITVECTOR_ADD, FLOATINGPOINT_ADD). --- examples/SimpleVC.java | 2 +- examples/api/cpp/combination.cpp | 2 +- examples/api/cpp/quickstart.cpp | 6 +-- examples/api/cpp/sygus-fun.cpp | 4 +- examples/api/cpp/sygus-grammar.cpp | 2 +- examples/api/cpp/sygus-inv.cpp | 2 +- examples/api/java/Combination.java | 2 +- examples/api/java/QuickStart.java | 6 +-- examples/api/java/SygusFun.java | 4 +- examples/api/java/SygusGrammar.java | 2 +- examples/api/java/SygusInv.java | 2 +- examples/api/python/combination.py | 2 +- examples/api/python/quickstart.py | 4 +- examples/api/python/sygus-fun.py | 4 +- examples/api/python/sygus-grammar.py | 2 +- examples/api/python/sygus-inv.py | 2 +- examples/nra-translate/smt2toisat.cpp | 2 +- examples/nra-translate/smt2tomathematica.cpp | 2 +- examples/nra-translate/smt2toqepcad.cpp | 2 +- examples/nra-translate/smt2toredlog.cpp | 2 +- examples/simple_vc_cxx.cpp | 2 +- src/api/cpp/cvc5.cpp | 4 +- src/api/cpp/cvc5_kind.h | 2 +- src/expr/dtype.h | 2 +- src/expr/kind_template.cpp | 3 +- src/expr/nary_term_util.cpp | 2 +- src/expr/node.h | 32 +++++++------- src/expr/node_algorithm.cpp | 2 +- src/expr/node_manager_template.h | 6 +-- src/expr/subtype_elim_node_converter.cpp | 2 +- src/expr/sygus_datatype.h | 2 +- src/parser/smt2/smt2.cpp | 4 +- src/parser/tptp/Tptp.g | 6 +-- src/preprocessing/passes/int_to_bv.cpp | 4 +- src/preprocessing/passes/miplib_trick.cpp | 2 +- src/preprocessing/passes/nl_ext_purify.cpp | 2 +- .../passes/pseudo_boolean_processor.cpp | 2 +- src/preprocessing/passes/real_to_int.cpp | 2 +- .../passes/unconstrained_simplifier.cpp | 2 +- src/printer/smt2/smt2_printer.cpp | 2 +- src/proof/alethe/alethe_post_processor.cpp | 2 +- src/proof/lfsc/lfsc_node_converter.cpp | 4 +- src/proof/lfsc/lfsc_post_processor.cpp | 2 +- src/theory/arith/arith_ite_utils.cpp | 2 +- src/theory/arith/arith_msum.cpp | 6 +-- src/theory/arith/arith_poly_norm.cpp | 4 +- src/theory/arith/arith_poly_norm.h | 2 +- src/theory/arith/arith_rewriter.cpp | 30 ++++++------- src/theory/arith/arith_utilities.h | 4 +- src/theory/arith/dio_solver.cpp | 2 +- src/theory/arith/kinds | 4 +- src/theory/arith/nl/ext/factoring_check.cpp | 5 +-- src/theory/arith/nl/ext/monomial.cpp | 2 +- src/theory/arith/nl/ext/proof_checker.cpp | 2 +- .../arith/nl/ext/tangent_plane_check.cpp | 2 +- src/theory/arith/nl/iand_utils.cpp | 2 +- src/theory/arith/nl/nl_model.cpp | 10 ++--- src/theory/arith/nl/poly_conversion.cpp | 8 ++-- .../nl/transcendental/exponential_solver.cpp | 4 +- .../arith/nl/transcendental/proof_checker.cpp | 14 +++---- .../arith/nl/transcendental/sine_solver.cpp | 6 +-- .../nl/transcendental/taylor_generator.cpp | 8 ++-- .../transcendental/transcendental_state.cpp | 2 +- src/theory/arith/normal_form.cpp | 16 ++++--- src/theory/arith/normal_form.h | 25 +++++++---- src/theory/arith/operator_elim.cpp | 14 +++---- src/theory/arith/proof_checker.cpp | 8 ++-- src/theory/arith/rewrites.h | 2 +- src/theory/arith/theory_arith_private.cpp | 19 +++++---- src/theory/bags/bag_reduction.cpp | 2 +- src/theory/bags/bags_rewriter.cpp | 2 +- src/theory/bags/card_solver.cpp | 2 +- src/theory/bags/inference_generator.cpp | 8 ++-- src/theory/builtin/kinds | 2 +- src/theory/bv/int_blaster.cpp | 6 +-- src/theory/bv/theory_bv_utils.cpp | 2 +- src/theory/datatypes/datatypes_rewriter.cpp | 2 +- src/theory/datatypes/sygus_extension.cpp | 2 +- src/theory/datatypes/sygus_simple_sym.cpp | 22 +++++----- src/theory/evaluator.cpp | 2 +- src/theory/quantifiers/bv_inverter.cpp | 2 +- .../cegqi/ceg_arith_instantiator.cpp | 26 ++++++------ .../quantifiers/cegqi/ceg_instantiator.cpp | 6 ++- .../ematching/inst_match_generator.cpp | 4 +- .../ematching/pattern_term_selector.cpp | 6 +-- .../ematching/relational_match_generator.cpp | 2 +- .../quantifiers/fmf/bounded_integers.cpp | 6 +-- .../quantifiers/quant_conflict_find.cpp | 9 ++-- src/theory/quantifiers/quantifiers_macros.cpp | 2 +- .../quantifiers/quantifiers_rewriter.cpp | 10 ++--- src/theory/quantifiers/relevant_domain.cpp | 6 +-- src/theory/quantifiers/sygus/cegis_unif.cpp | 2 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 14 +++---- .../quantifiers/sygus/sygus_grammar_norm.cpp | 18 ++++---- .../quantifiers/sygus/sygus_grammar_norm.h | 8 ++-- src/theory/quantifiers/sygus/type_info.cpp | 2 +- src/theory/quantifiers/sygus_sampler.cpp | 2 +- src/theory/quantifiers/term_database.h | 42 +++++++++---------- src/theory/quantifiers/term_util.cpp | 6 +-- src/theory/sets/theory_sets_rewriter.cpp | 2 +- src/theory/strings/arith_entail.cpp | 26 ++++++------ src/theory/strings/array_core_solver.cpp | 2 +- src/theory/strings/array_solver.cpp | 4 +- src/theory/strings/regexp_elim.cpp | 22 +++++----- src/theory/strings/sequences_rewriter.cpp | 20 ++++----- src/theory/strings/skolem_cache.cpp | 2 +- src/theory/strings/strings_entail.cpp | 2 +- src/theory/strings/strings_fmf.cpp | 2 +- src/theory/strings/term_registry.cpp | 2 +- .../strings/theory_strings_preprocess.cpp | 32 +++++++------- src/theory/theory_model.h | 2 +- src/util/statistics_stats.h | 2 +- test/unit/api/cpp/op_black.cpp | 6 +-- test/unit/api/cpp/op_white.cpp | 4 +- test/unit/api/cpp/solver_black.cpp | 20 ++++----- test/unit/api/cpp/term_black.cpp | 32 +++++++------- test/unit/api/java/OpTest.java | 2 +- test/unit/api/java/SolverTest.java | 18 ++++---- test/unit/api/java/TermTest.java | 32 +++++++------- test/unit/api/python/test_op.py | 4 +- test/unit/api/python/test_solver.py | 26 ++++++++---- test/unit/api/python/test_term.py | 32 +++++++------- test/unit/node/node_algorithm_black.cpp | 6 +-- test/unit/node/node_algorithms_black.cpp | 42 +++++++++---------- test/unit/node/node_black.cpp | 22 +++++----- test/unit/node/node_builder_black.cpp | 30 ++++++------- test/unit/node/node_white.cpp | 4 +- test/unit/theory/arith_poly_white.cpp | 38 ++++++++--------- test/unit/theory/sequences_rewriter_white.cpp | 22 +++++----- test/unit/theory/theory_arith_cad_white.cpp | 4 +- .../theory/theory_arith_rewriter_black.cpp | 2 +- test/unit/theory/theory_arith_white.cpp | 2 +- .../theory/theory_bags_rewriter_white.cpp | 4 +- test/unit/theory/theory_engine_white.cpp | 4 +- test/unit/theory/theory_int_opt_white.cpp | 2 +- test/unit/util/array_store_all_white.cpp | 2 +- 136 files changed, 543 insertions(+), 514 deletions(-) diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index 900d3710b..3a9eaf77d 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -44,7 +44,7 @@ public class SimpleVC Term two = slv.mkInteger(2); Term twox = slv.mkTerm(Kind.MULT, two, x); - Term twox_plus_y = slv.mkTerm(Kind.PLUS, twox, y); + Term twox_plus_y = slv.mkTerm(Kind.ADD, twox, y); Term three = slv.mkInteger(3); Term twox_plus_y_geq_3 = slv.mkTerm(Kind.GEQ, twox_plus_y, three); diff --git a/examples/api/cpp/combination.cpp b/examples/api/cpp/combination.cpp index 0cc9aa186..98393abe1 100644 --- a/examples/api/cpp/combination.cpp +++ b/examples/api/cpp/combination.cpp @@ -64,7 +64,7 @@ int main() // Terms Term f_x = slv.mkTerm(APPLY_UF, f, x); Term f_y = slv.mkTerm(APPLY_UF, f, y); - Term sum = slv.mkTerm(PLUS, f_x, f_y); + Term sum = slv.mkTerm(ADD, f_x, f_y); Term p_0 = slv.mkTerm(APPLY_UF, p, zero); Term p_f_y = slv.mkTerm(APPLY_UF, p, f_y); diff --git a/examples/api/cpp/quickstart.cpp b/examples/api/cpp/quickstart.cpp index 5bcb6bc66..35d9971cf 100644 --- a/examples/api/cpp/quickstart.cpp +++ b/examples/api/cpp/quickstart.cpp @@ -69,11 +69,11 @@ int main() Term one = solver.mkReal(1); // Next, we construct the term x + y - Term xPlusY = solver.mkTerm(PLUS, x, y); + Term xPlusY = solver.mkTerm(ADD, x, y); // Now we can define the constraints. // They use the operators +, <=, and <. - // In the API, these are denoted by PLUS, LEQ, and LT. + // In the API, these are denoted by ADD, LEQ, and LT. // A list of available operators is available in: // src/api/cpp/cvc5_kind.h Term constraint1 = solver.mkTerm(LT, zero, x); @@ -154,7 +154,7 @@ int main() solver.assertFormula(solver.mkTerm(LT, solver.mkInteger(0), a)); solver.assertFormula(solver.mkTerm(LT, solver.mkInteger(0), b)); solver.assertFormula( - solver.mkTerm(LT, solver.mkTerm(PLUS, a, b), solver.mkInteger(1))); + solver.mkTerm(LT, solver.mkTerm(ADD, a, b), solver.mkInteger(1))); solver.assertFormula(solver.mkTerm(LEQ, a, b)); // We check whether the revised assertion is satisfiable. diff --git a/examples/api/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp index e7a554177..f778af95b 100644 --- a/examples/api/cpp/sygus-fun.cpp +++ b/examples/api/cpp/sygus-fun.cpp @@ -82,7 +82,7 @@ int main() Term zero = slv.mkInteger(0); Term one = slv.mkInteger(1); - Term plus = slv.mkTerm(PLUS, start, start); + Term plus = slv.mkTerm(ADD, start, start); Term minus = slv.mkTerm(SUB, start, start); Term ite = slv.mkTerm(ITE, start_bool, start, start); @@ -124,7 +124,7 @@ int main() // (constraint (= (+ (max x y) (min x y)) // (+ x y))) slv.addSygusConstraint(slv.mkTerm( - EQUAL, slv.mkTerm(PLUS, max_x_y, min_x_y), slv.mkTerm(PLUS, varX, varY))); + EQUAL, slv.mkTerm(ADD, max_x_y, min_x_y), slv.mkTerm(ADD, varX, varY))); // print solutions if available if (slv.checkSynth().isUnsat()) diff --git a/examples/api/cpp/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp index b126c9410..ed0282bb9 100644 --- a/examples/api/cpp/sygus-grammar.cpp +++ b/examples/api/cpp/sygus-grammar.cpp @@ -76,7 +76,7 @@ int main() // define the rules Term zero = slv.mkInteger(0); Term neg_x = slv.mkTerm(NEG, x); - Term plus = slv.mkTerm(PLUS, x, start); + Term plus = slv.mkTerm(ADD, x, start); // create the grammar object Grammar g1 = slv.mkSygusGrammar({x}, {start}); diff --git a/examples/api/cpp/sygus-inv.cpp b/examples/api/cpp/sygus-inv.cpp index f658fa33a..9c976beef 100644 --- a/examples/api/cpp/sygus-inv.cpp +++ b/examples/api/cpp/sygus-inv.cpp @@ -69,7 +69,7 @@ int main() // (ite (< x 10) (= xp (+ x 1)) (= xp x)) Term ite = slv.mkTerm(ITE, slv.mkTerm(LT, x, ten), - slv.mkTerm(EQUAL, xp, slv.mkTerm(PLUS, x, one)), + slv.mkTerm(EQUAL, xp, slv.mkTerm(ADD, x, one)), slv.mkTerm(EQUAL, xp, x)); // define the pre-conditions, transition relations, and post-conditions diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index 03c43521a..e1eb77968 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -68,7 +68,7 @@ public class Combination // Terms Term f_x = slv.mkTerm(Kind.APPLY_UF, f, x); Term f_y = slv.mkTerm(Kind.APPLY_UF, f, y); - Term sum = slv.mkTerm(Kind.PLUS, f_x, f_y); + Term sum = slv.mkTerm(Kind.ADD, f_x, f_y); Term p_0 = slv.mkTerm(Kind.APPLY_UF, p, zero); Term p_f_y = slv.mkTerm(Kind.APPLY_UF, p, f_y); diff --git a/examples/api/java/QuickStart.java b/examples/api/java/QuickStart.java index a573b1966..ee169c490 100644 --- a/examples/api/java/QuickStart.java +++ b/examples/api/java/QuickStart.java @@ -70,11 +70,11 @@ public class QuickStart Term one = solver.mkReal(1); // Next, we construct the term x + y - Term xPlusY = solver.mkTerm(Kind.PLUS, x, y); + Term xPlusY = solver.mkTerm(Kind.ADD, x, y); // Now we can define the constraints. // They use the operators +, <=, and <. - // In the API, these are denoted by PLUS, LEQ, and LT. + // In the API, these are denoted by ADD, LEQ, and LT. // A list of available operators is available in: // src/api/cpp/cvc5_kind.h Term constraint1 = solver.mkTerm(Kind.LT, zero, x); @@ -145,7 +145,7 @@ public class QuickStart solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a)); solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b)); solver.assertFormula( - solver.mkTerm(Kind.LT, solver.mkTerm(Kind.PLUS, a, b), solver.mkInteger(1))); + solver.mkTerm(Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1))); solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b)); // We check whether the revised assertion is satisfiable. diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java index 05ed4cb91..31aecdc94 100644 --- a/examples/api/java/SygusFun.java +++ b/examples/api/java/SygusFun.java @@ -80,7 +80,7 @@ public class SygusFun Term zero = slv.mkInteger(0); Term one = slv.mkInteger(1); - Term plus = slv.mkTerm(PLUS, start, start); + Term plus = slv.mkTerm(ADD, start, start); Term minus = slv.mkTerm(SUB, start, start); Term ite = slv.mkTerm(ITE, start_bool, start, start); @@ -122,7 +122,7 @@ public class SygusFun // (constraint (= (+ (max x y) (min x y)) // (+ x y))) slv.addSygusConstraint( - slv.mkTerm(EQUAL, slv.mkTerm(PLUS, max_x_y, min_x_y), slv.mkTerm(PLUS, varX, varY))); + slv.mkTerm(EQUAL, slv.mkTerm(ADD, max_x_y, min_x_y), slv.mkTerm(ADD, varX, varY))); // print solutions if available if (slv.checkSynth().isUnsat()) diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java index d66378627..af8816a40 100644 --- a/examples/api/java/SygusGrammar.java +++ b/examples/api/java/SygusGrammar.java @@ -74,7 +74,7 @@ public class SygusGrammar // define the rules Term zero = slv.mkInteger(0); Term neg_x = slv.mkTerm(NEG, x); - Term plus = slv.mkTerm(PLUS, x, start); + Term plus = slv.mkTerm(ADD, x, start); // create the grammar object Grammar g1 = slv.mkSygusGrammar(new Term[] {x}, new Term[] {start}); diff --git a/examples/api/java/SygusInv.java b/examples/api/java/SygusInv.java index be1311318..226e8e61e 100644 --- a/examples/api/java/SygusInv.java +++ b/examples/api/java/SygusInv.java @@ -67,7 +67,7 @@ public class SygusInv // (ite (< x 10) (= xp (+ x 1)) (= xp x)) Term ite = slv.mkTerm(ITE, slv.mkTerm(LT, x, ten), - slv.mkTerm(EQUAL, xp, slv.mkTerm(PLUS, x, one)), + slv.mkTerm(EQUAL, xp, slv.mkTerm(ADD, x, one)), slv.mkTerm(EQUAL, xp, x)); // define the pre-conditions, transition relations, and post-conditions diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py index 57544b045..1f41c6913 100644 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -53,7 +53,7 @@ if __name__ == "__main__": # Terms f_x = slv.mkTerm(Kind.ApplyUf, f, x) f_y = slv.mkTerm(Kind.ApplyUf, f, y) - sum_ = slv.mkTerm(Kind.Plus, f_x, f_y) + sum_ = slv.mkTerm(Kind.Add, f_x, f_y) p_0 = slv.mkTerm(Kind.ApplyUf, p, zero) p_f_y = slv.mkTerm(Kind.ApplyUf, p, f_y) diff --git a/examples/api/python/quickstart.py b/examples/api/python/quickstart.py index 6846eb503..dc5e36683 100644 --- a/examples/api/python/quickstart.py +++ b/examples/api/python/quickstart.py @@ -64,7 +64,7 @@ if __name__ == "__main__": one = solver.mkReal(1); # Next, we construct the term x + y - xPlusY = solver.mkTerm(Kind.Plus, x, y); + xPlusY = solver.mkTerm(Kind.Add, x, y); # Now we can define the constraints. # They use the operators +, <=, and <. @@ -135,7 +135,7 @@ if __name__ == "__main__": solver.assertFormula(solver.mkTerm(Kind.Lt, solver.mkInteger(0), a)); solver.assertFormula(solver.mkTerm(Kind.Lt, solver.mkInteger(0), b)); solver.assertFormula( - solver.mkTerm(Kind.Lt, solver.mkTerm(Kind.Plus, a, b), solver.mkInteger(1))); + solver.mkTerm(Kind.Lt, solver.mkTerm(Kind.Add, a, b), solver.mkInteger(1))); solver.assertFormula(solver.mkTerm(Kind.Leq, a, b)); # We check whether the revised assertion is satisfiable. diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index 939e1f9ed..2f6417e35 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -45,7 +45,7 @@ if __name__ == "__main__": zero = slv.mkInteger(0) one = slv.mkInteger(1) - plus = slv.mkTerm(Kind.Plus, start, start) + plus = slv.mkTerm(Kind.Add, start, start) minus = slv.mkTerm(Kind.Sub, start, start) ite = slv.mkTerm(Kind.Ite, start_bool, start, start) @@ -87,7 +87,7 @@ if __name__ == "__main__": # (constraint (= (+ (max x y) (min x y)) # (+ x y))) slv.addSygusConstraint(slv.mkTerm( - Kind.Equal, slv.mkTerm(Kind.Plus, max_x_y, min_x_y), slv.mkTerm(Kind.Plus, varX, varY))) + Kind.Equal, slv.mkTerm(Kind.Add, max_x_y, min_x_y), slv.mkTerm(Kind.Add, varX, varY))) # print solutions if available if (slv.checkSynth().isUnsat()): diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index d513dc139..41adad822 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -43,7 +43,7 @@ if __name__ == "__main__": # define the rules zero = slv.mkInteger(0) neg_x = slv.mkTerm(Kind.Neg, x) - plus = slv.mkTerm(Kind.Plus, x, start) + plus = slv.mkTerm(Kind.Add, x, start) # create the grammar object g1 = slv.mkSygusGrammar({x}, {start}) diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py index 1c2c14535..249952a9e 100644 --- a/examples/api/python/sygus-inv.py +++ b/examples/api/python/sygus-inv.py @@ -44,7 +44,7 @@ if __name__ == "__main__": # (ite (< x 10) (= xp (+ x 1)) (= xp x)) ite = slv.mkTerm(Kind.Ite, slv.mkTerm(Kind.Lt, x, ten), - slv.mkTerm(Kind.Equal, xp, slv.mkTerm(Kind.Plus, x, one)), + slv.mkTerm(Kind.Equal, xp, slv.mkTerm(Kind.Add, x, one)), slv.mkTerm(Kind.Equal, xp, x)) # define the pre-conditions, transition relations, and post-conditions diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index 9a960b372..9cde61d28 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -112,7 +112,7 @@ void translate_to_isat_term(const map& variables, const Expr& te } else { switch (term.getKind()) { - case kind::PLUS: + case kind::ADD: cout << "("; first = true; for (unsigned i = 0; i < n; ++ i) { diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index 5de9415f7..de91cb95e 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -111,7 +111,7 @@ void translate_to_mathematica_term(const map& variables, const E } else { switch (term.getKind()) { - case kind::PLUS: + case kind::ADD: cout << "("; first = true; for (unsigned i = 0; i < n; ++ i) { diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index 8f4350d58..1fc1a3b47 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -115,7 +115,7 @@ void translate_to_qepcad_term(const std::map& variables, } else { switch (term.getKind()) { - case kind::PLUS: + case kind::ADD: cout << "("; first = true; for (unsigned i = 0; i < n; ++ i) { diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index 0aa95a8d2..0d2d536b4 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -115,7 +115,7 @@ void translate_to_redlog_term(const map& variables, const Expr& } else { switch (term.getKind()) { - case kind::PLUS: + case kind::ADD: cout << "("; first = true; for (unsigned i = 0; i < n; ++ i) { diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 1c0663a00..fa3602540 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -39,7 +39,7 @@ int main() { Term two = slv.mkInteger(2); Term twox = slv.mkTerm(Kind::MULT, two, x); - Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y); + Term twox_plus_y = slv.mkTerm(Kind::ADD, twox, y); Term three = slv.mkInteger(3); Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three); diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 9b17dbc7a..d46b8a971 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -130,7 +130,7 @@ const static std::unordered_map s_kinds{ {CARDINALITY_CONSTRAINT, cvc5::Kind::CARDINALITY_CONSTRAINT}, {HO_APPLY, cvc5::Kind::HO_APPLY}, /* Arithmetic ---------------------------------------------------------- */ - {PLUS, cvc5::Kind::PLUS}, + {ADD, cvc5::Kind::ADD}, {MULT, cvc5::Kind::MULT}, {IAND, cvc5::Kind::IAND}, {POW2, cvc5::Kind::POW2}, @@ -412,7 +412,7 @@ const static std::unordered_map {cvc5::Kind::CARDINALITY_CONSTRAINT, CARDINALITY_CONSTRAINT}, {cvc5::Kind::HO_APPLY, HO_APPLY}, /* Arithmetic ------------------------------------------------------ */ - {cvc5::Kind::PLUS, PLUS}, + {cvc5::Kind::ADD, ADD}, {cvc5::Kind::MULT, MULT}, {cvc5::Kind::IAND, IAND}, {cvc5::Kind::POW2, POW2}, diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 7644cff4d..1609fb221 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -348,7 +348,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - PLUS, + ADD, /** * Arithmetic multiplication. * diff --git a/src/expr/dtype.h b/src/expr/dtype.h index 4f54f0af7..210662ce4 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -177,7 +177,7 @@ class DType * @param cargs the arguments of the constructor. * It should be the case that cargs are sygus datatypes that * encode the arguments of op. For example, a sygus constructor - * with op = PLUS should be such that cargs.size()>=2 and + * with op = ADD should be such that cargs.size()>=2 and * the sygus type of cargs[i] is Real/Int for each i. * @param weight denotes the value added by the constructor when computing the * size of datatype terms. Passing a value < 0 denotes the default weight for diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp index 49f815b68..9c6fc6d0a 100644 --- a/src/expr/kind_template.cpp +++ b/src/expr/kind_template.cpp @@ -56,8 +56,7 @@ bool isAssociative(::cvc5::Kind k) case kind::AND: case kind::OR: case kind::MULT: - case kind::PLUS: - return true; + case kind::ADD: return true; default: return false; diff --git a/src/expr/nary_term_util.cpp b/src/expr/nary_term_util.cpp index 500b45a81..59ed342f2 100644 --- a/src/expr/nary_term_util.cpp +++ b/src/expr/nary_term_util.cpp @@ -119,7 +119,7 @@ Node getNullTerminator(Kind k, TypeNode tn) case OR: nullTerm = nm->mkConst(false); break; case AND: case SEP_STAR: nullTerm = nm->mkConst(true); break; - case PLUS: nullTerm = nm->mkConstRealOrInt(tn, Rational(0)); break; + case ADD: nullTerm = nm->mkConstRealOrInt(tn, Rational(0)); break; case MULT: case NONLINEAR_MULT: nullTerm = nm->mkConstRealOrInt(tn, Rational(1)); diff --git a/src/expr/node.h b/src/expr/node.h index 3a4706e1e..5fc22b3d3 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -690,10 +690,10 @@ public: * Returns the iterator pointing to the first child, if the node's * kind is the same as the parameter, otherwise returns the iterator * pointing to the node itself. This is useful if you want to - * pretend to iterate over a "unary" PLUS, for instance, since unary - * PLUSes don't exist---begin(PLUS) will give an iterator over the - * children if the node's a PLUS node, otherwise give an iterator - * over the node itself, as if it were a unary PLUS. + * pretend to iterate over a "unary" ADD, for instance, since unary + * PLUSes don't exist---begin(ADD) will give an iterator over the + * children if the node's an ADD node, otherwise give an iterator + * over the node itself, as if it were a unary ADD. * @param kind the kind to match * @return the kinded_iterator iterating over this Node (if its kind * is not the passed kind) or its children @@ -708,10 +708,10 @@ public: * beyond the last one), if the node's kind is the same as the * parameter, otherwise returns the iterator pointing to the * one-of-the-node-itself. This is useful if you want to pretend to - * iterate over a "unary" PLUS, for instance, since unary PLUSes - * don't exist---begin(PLUS) will give an iterator over the children - * if the node's a PLUS node, otherwise give an iterator over the - * node itself, as if it were a unary PLUS. + * iterate over a "unary" ADD, for instance, since unary PLUSes + * don't exist---begin(ADD) will give an iterator over the children + * if the node's an ADD node, otherwise give an iterator over the + * node itself, as if it were a unary ADD. * @param kind the kind to match * @return the kinded_iterator pointing off-the-end of this Node (if * its kind is not the passed kind) or off-the-end of its children @@ -766,10 +766,10 @@ public: * Returns the iterator pointing to the first child, if the node's * kind is the same as the parameter, otherwise returns the iterator * pointing to the node itself. This is useful if you want to - * pretend to iterate over a "unary" PLUS, for instance, since unary - * PLUSes don't exist---begin(PLUS) will give an iterator over the - * children if the node's a PLUS node, otherwise give an iterator - * over the node itself, as if it were a unary PLUS. + * pretend to iterate over a "unary" ADD, for instance, since unary + * PLUSes don't exist---begin(ADD) will give an iterator over the + * children if the node's an ADD node, otherwise give an iterator + * over the node itself, as if it were a unary ADD. * @param kind the kind to match * @return the kinded_iterator iterating over this Node (if its kind * is not the passed kind) or its children @@ -784,10 +784,10 @@ public: * beyond the last one), if the node's kind is the same as the * parameter, otherwise returns the iterator pointing to the * one-of-the-node-itself. This is useful if you want to pretend to - * iterate over a "unary" PLUS, for instance, since unary PLUSes - * don't exist---begin(PLUS) will give an iterator over the children - * if the node's a PLUS node, otherwise give an iterator over the - * node itself, as if it were a unary PLUS. + * iterate over a "unary" ADD, for instance, since unary PLUSes + * don't exist---begin(ADD) will give an iterator over the children + * if the node's an ADD node, otherwise give an iterator over the + * node itself, as if it were a unary ADD. * @param kind the kind to match * @return the kinded_iterator pointing off-the-end of this Node (if * its kind is not the passed kind) or off-the-end of its children diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index a7bea656a..7a23d67c9 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -838,7 +838,7 @@ bool match(Node x, Node y, std::unordered_map& subs) // equal // we compare operators instead of kinds because different terms may have // the same kind (both `(id x)` and `(square x)` have kind APPLY_UF) - // since many builtin operators like `PLUS` allow arbitrary number of + // since many builtin operators like `ADD` allow arbitrary number of // arguments, we also need to check if the two subterms have the same // number of children if (curr.first.getNumChildren() != curr.second.getNumChildren() diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h index 83cb21cbb..f992b3910 100644 --- a/src/expr/node_manager_template.h +++ b/src/expr/node_manager_template.h @@ -1037,10 +1037,10 @@ class NodeManager /** * A set of operator singletons (w.r.t. to this NodeManager * instance) for operators. Conceptually, Nodes with kind, say, - * PLUS, are APPLYs of a PLUS operator to arguments. This array - * holds the set of operators for these things. A PLUS operator is + * ADD, are APPLYs of a ADD operator to arguments. This array + * holds the set of operators for these things. A ADD operator is * a Node with kind "BUILTIN", and if you call - * plusOperator->getConst(), you get kind::PLUS back. + * plusOperator->getConst(), you get kind::ADD back. */ Node d_operators[kind::LAST_KIND]; diff --git a/src/expr/subtype_elim_node_converter.cpp b/src/expr/subtype_elim_node_converter.cpp index fd888a0f2..00a9fdd3a 100644 --- a/src/expr/subtype_elim_node_converter.cpp +++ b/src/expr/subtype_elim_node_converter.cpp @@ -30,7 +30,7 @@ Node SubtypeElimNodeConverter::postConvert(Node n) { Kind k = n.getKind(); bool convertToRealChildren = false; - if (k == PLUS || k == MULT || k == NONLINEAR_MULT) + if (k == ADD || k == MULT || k == NONLINEAR_MULT) { convertToRealChildren = isRealTypeStrict(n.getType()); } diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h index fa3fce5b2..53c028185 100644 --- a/src/expr/sygus_datatype.h +++ b/src/expr/sygus_datatype.h @@ -82,7 +82,7 @@ class SygusDatatype * * It should be the case that argTypes are sygus datatype types (possibly * unresolved) that encode the arguments of the builtin operator. That is, - * if op is the builtin PLUS operator, then argTypes could contain 2+ + * if op is the builtin ADD operator, then argTypes could contain 2+ * sygus datatype types that encode integer. */ void addConstructor(Node op, diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3618d38cf..1c3ea84df 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -24,6 +24,8 @@ // ANTLR defines these, which is really bad! #undef true #undef false +// ANTLR pulls in arpa/nameser_compat.h which defines this (again, bad!) +#undef ADD namespace cvc5 { namespace parser { @@ -41,7 +43,7 @@ Smt2::Smt2(api::Solver* solver, Smt2::~Smt2() {} void Smt2::addArithmeticOperators() { - addOperator(api::PLUS, "+"); + addOperator(api::ADD, "+"); addOperator(api::SUB, "-"); // api::SUB is converted to api::NEG if there is only a single operand Parser::addOperator(api::NEG); diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 1c9b2092c..45e71b271 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -571,7 +571,7 @@ definedFun[cvc5::ParseOp& p] } | '$sum' { - p.d_kind = api::PLUS; + p.d_kind = api::ADD; } | '$difference' { @@ -688,12 +688,12 @@ definedFun[cvc5::ParseOp& p] MK_TERM(api::GT, decPart, SOLVER->mkReal(1, 2)), // if decPart > 0.5, round up MK_TERM(api::TO_INTEGER, - MK_TERM(api::PLUS, n, SOLVER->mkReal(1))), + MK_TERM(api::ADD, n, SOLVER->mkReal(1))), // if decPart == 0.5, round to nearest even integer: // result is: to_int(n/2 + .5) * 2 MK_TERM(api::MULT, MK_TERM(api::TO_INTEGER, - MK_TERM(api::PLUS, + MK_TERM(api::ADD, MK_TERM(api::DIVISION, n, SOLVER->mkReal(2)), diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 4927247bb..b5b25b2f3 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -69,7 +69,7 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) result = current; } else if (current.getNumChildren() > 2 - && (current.getKind() == kind::PLUS + && (current.getKind() == kind::ADD || current.getKind() == kind::MULT || current.getKind() == kind::NONLINEAR_MULT)) { @@ -149,7 +149,7 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache) { switch (newKind) { - case kind::PLUS: + case kind::ADD: Assert(children.size() == 2); newKind = kind::BITVECTOR_ADD; max = max + 1; diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 1be5ee81b..f38567965 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -561,7 +561,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( Node sum; if (pos.getKind() == kind::AND) { - NodeBuilder sumb(kind::PLUS); + NodeBuilder sumb(kind::ADD); for (size_t jj = 0; jj < pos.getNumChildren(); ++jj) { sumb << nm->mkNode( diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index aa7805284..ad1821bf4 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -60,7 +60,7 @@ Node NlExtPurify::purifyNlTerms(TNode n, Node ret = n; if (n.getNumChildren() > 0) { - if (beneathMult && (n.getKind() == kind::PLUS || n.getKind() == kind::SUB)) + if (beneathMult && (n.getKind() == kind::ADD || n.getKind() == kind::SUB)) { // don't do it if it rewrites to a constant Node nr = rewrite(n); diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index eae1d00fd..f6095ee9c 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.cpp +++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp @@ -72,7 +72,7 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated) return false; } // don't bother matching on anything other than + on the left hand side - if (l.getKind() != kind::PLUS) + if (l.getKind() != kind::ADD) { Debug("pbs::rewrites") << "not plus" << assertion << std::endl; return false; diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index ef9077770..9b84013cd 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -134,7 +134,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va Node sumt = sum.empty() ? nm->mkConstInt(Rational(0)) - : (sum.size() == 1 ? sum[0] : nm->mkNode(kind::PLUS, sum)); + : (sum.size() == 1 ? sum[0] : nm->mkNode(kind::ADD, sum)); ret = nm->mkNode( ret_lit.getKind(), sumt, nm->mkConstInt(Rational(0))); if (!ret_pol) diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 31a888dd0..b31e2e865 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -447,7 +447,7 @@ void UnconstrainedSimplifier::processUnconstrained() // N-ary operators returning same type requiring at least one child to // be unconstrained - case kind::PLUS: + case kind::ADD: case kind::SUB: if (current.getType().isInteger() && !parent.getType().isInteger()) { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 173247b1c..dd74f0071 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -989,7 +989,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::WITNESS: return "witness"; // arith theory - case kind::PLUS: return "+"; + case kind::ADD: return "+"; case kind::MULT: case kind::NONLINEAR_MULT: return "*"; case kind::IAND: return "iand"; diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 4d1a3b5a6..759974687 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -428,7 +428,7 @@ bool AletheProofPostprocessCallback::update(Node res, vrule = AletheRule::UNARY_MINUS_SIMPLIFY; break; } - case kind::PLUS: + case kind::ADD: { vrule = AletheRule::SUM_SIMPLIFY; break; diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index ffde0b274..8edbb7dc7 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -428,7 +428,7 @@ Node LfscNodeConverter::postConvert(Node n) // check whether we are also changing the operator name, in which case // we build a binary uninterpreted function opc Node opc; - if (k == PLUS || k == MULT || k == NONLINEAR_MULT) + if (k == ADD || k == MULT || k == NONLINEAR_MULT) { std::stringstream opName; // currently allow subtyping @@ -982,7 +982,7 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply) opName << "f_"; } // all arithmetic kinds must explicitly deal with real vs int subtyping - if (k == PLUS || k == MULT || k == NONLINEAR_MULT || k == GEQ || k == GT + if (k == ADD || k == MULT || k == NONLINEAR_MULT || k == GEQ || k == GT || k == LEQ || k == LT || k == SUB || k == DIVISION || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == NEG || k == POW) diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp index 33004e81f..3e5aa5f8a 100644 --- a/src/proof/lfsc/lfsc_post_processor.cpp +++ b/src/proof/lfsc/lfsc_post_processor.cpp @@ -334,7 +334,7 @@ bool LfscProofPostprocessCallback::update(Node res, case PfRule::ARITH_SUM_UB: { // proof of null terminator base 0 = 0 - Node zero = d_tproc.getNullTerminator(PLUS); + Node zero = d_tproc.getNullTerminator(ADD); Node cur = zero.eqNode(zero); cdp->addStep(cur, PfRule::REFL, {}, {zero}); for (size_t i = 0, size = children.size(); i < size; i++) diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 36cd18aa1..029b74ed0 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -80,7 +80,7 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ return rite; }else{ Node constantite = rc.iteNode(d_constants[t], d_constants[e]); - Node sum = nm->mkNode(kind::PLUS, vpite, constantite); + Node sum = nm->mkNode(kind::ADD, vpite, constantite); d_reduceVar[n] = sum; d_constants[n] = constantite; d_varParts[n] = vpite; diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index 0621c1391..db08f3af0 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -65,7 +65,7 @@ bool ArithMSum::getMonomial(Node n, std::map& msum) bool ArithMSum::getMonomialSum(Node n, std::map& msum) { - if (n.getKind() == PLUS) + if (n.getKind() == ADD) { for (Node nc : n) { @@ -149,7 +149,7 @@ Node ArithMSum::mkNode(TypeNode tn, const std::map& msum) children.push_back(m); } return children.size() > 1 - ? nm->mkNode(PLUS, children) + ? nm->mkNode(ADD, children) : (children.size() == 1 ? children[0] : nm->mkConstRealOrInt(tn, Rational(0))); } @@ -188,7 +188,7 @@ int ArithMSum::isolate( } val = children.size() > 1 - ? nm->mkNode(PLUS, children) + ? nm->mkNode(ADD, children) : (children.size() == 1 ? children[0] : nm->mkConstRealOrInt(vtn, Rational(0))); if (!r.isOne() && !r.isNegativeOne()) diff --git a/src/theory/arith/arith_poly_norm.cpp b/src/theory/arith/arith_poly_norm.cpp index 99a38dd58..c4c8f765e 100644 --- a/src/theory/arith/arith_poly_norm.cpp +++ b/src/theory/arith/arith_poly_norm.cpp @@ -201,7 +201,7 @@ PolyNorm PolyNorm::mkPolyNorm(TNode n) visited[cur].addMonomial(null, r); } } - else if (k == PLUS || k == SUB || k == NEG || k == MULT + else if (k == ADD || k == SUB || k == NEG || k == MULT || k == NONLINEAR_MULT) { visited[cur] = PolyNorm(); @@ -224,7 +224,7 @@ PolyNorm PolyNorm::mkPolyNorm(TNode n) PolyNorm& ret = visited[cur]; switch (k) { - case PLUS: + case ADD: case SUB: case NEG: case MULT: diff --git a/src/theory/arith/arith_poly_norm.h b/src/theory/arith/arith_poly_norm.h index c36da60be..58f5f6c7a 100644 --- a/src/theory/arith/arith_poly_norm.h +++ b/src/theory/arith/arith_poly_norm.h @@ -58,7 +58,7 @@ class PolyNorm bool isEqual(const PolyNorm& p) const; /** * Make polynomial from real term n. This method normalizes applications - * of operators PLUS, SUB, NEG, MULT, and NONLINEAR_MULT only. + * of operators ADD, SUB, NEG, MULT, and NONLINEAR_MULT only. */ static PolyNorm mkPolyNorm(TNode n); /** Do a and b normalize to the same polynomial? */ diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 82cc5878f..7d4bd4b83 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -367,9 +367,8 @@ RewriteResponse ArithRewriter::rewriteSub(TNode t) return RewriteResponse(REWRITE_DONE, nm->mkConstRealOrInt(t.getType(), Rational(0))); } - return RewriteResponse( - REWRITE_AGAIN_FULL, - nm->mkNode(Kind::PLUS, t[0], makeUnaryMinusNode(t[1]))); + return RewriteResponse(REWRITE_AGAIN_FULL, + nm->mkNode(Kind::ADD, t[0], makeUnaryMinusNode(t[1]))); } RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre) @@ -410,7 +409,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::NEG: return rewriteNeg(t, true); case kind::DIVISION: case kind::DIVISION_TOTAL: return rewriteDiv(t, true); - case kind::PLUS: return preRewritePlus(t); + case kind::ADD: return preRewritePlus(t); case kind::MULT: case kind::NONLINEAR_MULT: return preRewriteMult(t); case kind::IAND: return RewriteResponse(REWRITE_DONE, t); @@ -458,7 +457,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ case kind::NEG: return rewriteNeg(t, false); case kind::DIVISION: case kind::DIVISION_TOTAL: return rewriteDiv(t, false); - case kind::PLUS: return postRewritePlus(t); + case kind::ADD: return postRewritePlus(t); case kind::MULT: case kind::NONLINEAR_MULT: return postRewriteMult(t); case kind::IAND: return postRewriteIAnd(t); @@ -541,12 +540,12 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ RewriteResponse ArithRewriter::preRewritePlus(TNode t){ - Assert(t.getKind() == kind::PLUS); + Assert(t.getKind() == kind::ADD); return RewriteResponse(REWRITE_DONE, expr::algorithm::flatten(t)); } RewriteResponse ArithRewriter::postRewritePlus(TNode t){ - Assert(t.getKind() == kind::PLUS); + Assert(t.getKind() == kind::ADD); Assert(t.getNumChildren() > 1); { @@ -619,7 +618,7 @@ RewriteResponse ArithRewriter::postRewritePlus(TNode t){ } return RewriteResponse( REWRITE_DONE, - nm->mkNode(Kind::PLUS, nm->mkRealAlgebraicNumber(ran), poly.getNode())); + nm->mkNode(Kind::ADD, nm->mkRealAlgebraicNumber(ran), poly.getNode())); } RewriteResponse ArithRewriter::preRewriteMult(TNode node) @@ -779,7 +778,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { return RewriteResponse(REWRITE_DONE, t); } } - else if (t[0].getKind() == kind::PLUS) + else if (t[0].getKind() == kind::ADD) { std::vector product; for (const Node tc : t[0]) @@ -850,16 +849,19 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { //add/substract 2*pi beyond scope Rational ra_div_two = (r_abs + rone) / rtwo; Node new_pi_factor; - if( r.sgn()==1 ){ + if (r.sgn() == 1) + { new_pi_factor = nm->mkConstReal(r - rtwo * ra_div_two.floor()); - }else{ + } + else + { Assert(r.sgn() == -1); new_pi_factor = nm->mkConstReal(r + rtwo * ra_div_two.floor()); } Node new_arg = nm->mkNode(kind::MULT, new_pi_factor, pi); if (!rem.isNull()) { - new_arg = nm->mkNode(kind::PLUS, new_arg, rem); + new_arg = nm->mkNode(kind::ADD, new_arg, rem); } // sin( 2*n*PI + x ) = sin( x ) return RewriteResponse(REWRITE_AGAIN_FULL, @@ -1189,7 +1191,7 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre) // (mod (mod x c) c) --> (mod x c) return returnRewrite(t, t[0], Rewrite::MOD_OVER_MOD); } - else if (k0 == kind::NONLINEAR_MULT || k0 == kind::MULT || k0 == kind::PLUS) + else if (k0 == kind::NONLINEAR_MULT || k0 == kind::MULT || k0 == kind::ADD) { // can drop all std::vector newChildren; @@ -1207,7 +1209,7 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre) if (childChanged) { // (mod (op ... (mod x c) ...) c) ---> (mod (op ... x ...) c) where - // op is one of { NONLINEAR_MULT, MULT, PLUS }. + // op is one of { NONLINEAR_MULT, MULT, ADD }. Node ret = nm->mkNode(k0, newChildren); ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, ret, t[1]); return returnRewrite(t, ret, Rewrite::MOD_CHILD_MOD); diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 1e844f829..c8746d6c9 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -195,7 +195,7 @@ inline Node negateConjunctionAsClause(TNode conjunction){ inline Node maybeUnaryConvert(NodeBuilder& builder) { Assert(builder.getKind() == kind::OR || builder.getKind() == kind::AND - || builder.getKind() == kind::PLUS || builder.getKind() == kind::MULT); + || builder.getKind() == kind::ADD || builder.getKind() == kind::MULT); Assert(builder.getNumChildren() >= 1); if(builder.getNumChildren() == 1){ return builder[0]; @@ -227,7 +227,7 @@ inline Node getIdentityType(const TypeNode& tn, Kind k) { switch (k) { - case kind::PLUS: return NodeManager::currentNM()->mkConstRealOrInt(tn, 0); + case kind::ADD: return NodeManager::currentNM()->mkConstRealOrInt(tn, 0); case kind::MULT: case kind::NONLINEAR_MULT: return NodeManager::currentNM()->mkConstRealOrInt(tn, 1); diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index af3d8a692..de8ee8477 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -671,7 +671,7 @@ std::pair DioSolver::decomposeIndex( //We need to handle both cases seperately to ensure termination. Node qr = SumPair::computeQR(si, a.getValue().getNumerator()); - Assert(qr.getKind() == kind::PLUS); + Assert(qr.getKind() == kind::ADD); Assert(qr.getNumChildren() == 2); SumPair q = SumPair::parseSumPair(qr[0]); SumPair r = SumPair::parseSumPair(qr[1]); diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 5d96e019f..cd26d8033 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -12,7 +12,7 @@ properties check propagate ppStaticLearn presolve notifyRestart rewriter ::cvc5::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" -operator PLUS 2: "arithmetic addition (N-ary)" +operator ADD 2: "arithmetic addition (N-ary)" operator MULT 2: "arithmetic multiplication (N-ary)" operator NONLINEAR_MULT 2: "synonym for MULT" operator SUB 2 "arithmetic binary subtraction operator" @@ -118,7 +118,7 @@ operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this # This way, we avoid having 2 nested TO_REAL nodess as a result of Solver::mkTerm(TO_REAL, Solver::mkReal(int val)) operator CAST_TO_REAL 1 "cast term to real same as TO_REAL, but it is used internally, whereas TO_REAL is accessible in the API" -typerule PLUS ::cvc5::theory::arith::ArithOperatorTypeRule +typerule ADD ::cvc5::theory::arith::ArithOperatorTypeRule typerule MULT ::cvc5::theory::arith::ArithOperatorTypeRule typerule NONLINEAR_MULT ::cvc5::theory::arith::ArithOperatorTypeRule typerule SUB ::cvc5::theory::arith::ArithOperatorTypeRule diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 32b630fa8..51b589351 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -123,7 +123,7 @@ void FactoringCheck::check(const std::vector& asserts, { continue; } - Node sum = nm->mkNode(Kind::PLUS, itf->second); + Node sum = nm->mkNode(Kind::ADD, itf->second); sum = rewrite(sum); Trace("nl-ext-factor") << "* Factored sum for " << x << " : " << sum << std::endl; @@ -150,8 +150,7 @@ void FactoringCheck::check(const std::vector& asserts, itm->second, itm->first.isNull() ? d_one : itm->first)); } } - Node polyn = - poly.size() == 1 ? poly[0] : nm->mkNode(Kind::PLUS, poly); + Node polyn = poly.size() == 1 ? poly[0] : nm->mkNode(Kind::ADD, poly); Trace("nl-ext-factor") << "...factored polynomial : " << polyn << std::endl; Node zero = nm->mkConstRealOrInt(polyn.getType(), Rational(0)); diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp index d71b41da6..9d052f0b2 100644 --- a/src/theory/arith/nl/ext/monomial.cpp +++ b/src/theory/arith/nl/ext/monomial.cpp @@ -158,7 +158,7 @@ void MonomialDb::registerMonomial(Node n) } else { - Assert(k != PLUS && k != MULT); + Assert(k != ADD && k != MULT); d_m_exp[n][n] = 1; d_m_vlist[n].push_back(n); d_m_degree[n] = 1; diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index fe134abb4..bcfd1f2d1 100644 --- a/src/theory/arith/nl/ext/proof_checker.cpp +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -137,7 +137,7 @@ Node ExtProofRuleChecker::checkInternal(PfRule id, int sgn = args[5].getConst().getNumerator().sgn(); Assert(sgn == -1 || sgn == 1); Node tplane = nm->mkNode(Kind::SUB, - nm->mkNode(Kind::PLUS, + nm->mkNode(Kind::ADD, nm->mkNode(Kind::MULT, b, x), nm->mkNode(Kind::MULT, a, y)), nm->mkNode(Kind::MULT, a, b)); diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 4ec1f2ca2..e7c42a830 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -120,7 +120,7 @@ void TangentPlaneCheck::check(bool asWaitingLemmas) // tangent plane Node tplane = nm->mkNode(Kind::SUB, - nm->mkNode(Kind::PLUS, + nm->mkNode(Kind::ADD, nm->mkNode(Kind::MULT, b_v, a), nm->mkNode(Kind::MULT, a_v, b)), nm->mkNode(Kind::MULT, a_v, b_v)); diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index d64c19963..9c9486446 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -152,7 +152,7 @@ Node IAndUtils::createSumNode(Node x, Node sumPart = createITEFromTable(xExtract, yExtract, granularity, table); // append the current block to the sum sumNode = - nm->mkNode(kind::PLUS, + nm->mkNode(kind::ADD, sumNode, nm->mkNode(kind::MULT, pow2(i * granularity), sumPart)); } diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 1f50290c1..edd00a6dd 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -208,7 +208,7 @@ bool NlModel::checkModel(const std::vector& assertions, if (cur.getType().isRealOrInt() && !cur.isConst()) { Kind k = cur.getKind(); - if (k != MULT && k != PLUS && k != NONLINEAR_MULT + if (k != MULT && k != ADD && k != NONLINEAR_MULT && !isTranscendentalKind(k)) { // if we have not set an approximate bound for it @@ -644,7 +644,7 @@ bool NlModel::simpleCheckModelLit(Node lit) Node invalid_vsum = vs_invalid.empty() ? d_zero : (vs_invalid.size() == 1 ? vs_invalid[0] - : nm->mkNode(PLUS, vs_invalid)); + : nm->mkNode(ADD, vs_invalid)); // substitution to try Subs qsub; for (const Node& v : vs) @@ -667,7 +667,7 @@ bool NlModel::simpleCheckModelLit(Node lit) if (it != v_b.end()) { b = it->second; - t = nm->mkNode(PLUS, t, nm->mkNode(MULT, b, v)); + t = nm->mkNode(ADD, t, nm->mkNode(MULT, b, v)); } t = rewrite(t); Trace("nl-ext-cms-debug") << "Trying to find min/max for quadratic " @@ -986,7 +986,7 @@ bool NlModel::simpleCheckModelMsum(const std::map& msum, bool pol) Node bound; if (sum_bound.size() > 1) { - bound = nm->mkNode(kind::PLUS, sum_bound); + bound = nm->mkNode(kind::ADD, sum_bound); } else if (sum_bound.size() == 1) { @@ -1072,7 +1072,7 @@ void NlModel::getModelValueRepair( // witness is the midpoint witness = nm->mkNode(MULT, nm->mkConst(CONST_RATIONAL, Rational(1, 2)), - nm->mkNode(PLUS, l, u)); + nm->mkNode(ADD, l, u)); witness = rewrite(witness); Trace("nl-model") << v << " witness is " << witness << std::endl; } diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 4a636ac60..43c3d152d 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -81,7 +81,7 @@ cvc5::Node as_cvc_upolynomial(const poly::UPolynomial& p, const cvc5::Node& var) Node coeff = nm->mkConst(CONST_RATIONAL, poly_utils::toRational(coeffs[i])); Node term = nm->mkNode(Kind::MULT, coeff, monomial); - res = nm->mkNode(Kind::PLUS, res, term); + res = nm->mkNode(Kind::ADD, res, term); } monomial = nm->mkNode(Kind::NONLINEAR_MULT, monomial, var); } @@ -108,7 +108,7 @@ poly::UPolynomial as_poly_upolynomial_impl(const cvc5::Node& n, denominator = poly_utils::toInteger(r.getDenominator()); return poly::UPolynomial(poly_utils::toInteger(r.getNumerator())); } - case Kind::PLUS: + case Kind::ADD: { poly::UPolynomial res; poly::Integer denom; @@ -166,7 +166,7 @@ poly::Polynomial as_poly_polynomial_impl(const cvc5::Node& n, denominator = poly_utils::toInteger(r.getDenominator()); return poly::Polynomial(poly_utils::toInteger(r.getNumerator())); } - case Kind::PLUS: + case Kind::ADD: { poly::Polynomial res; poly::Integer denom; @@ -273,7 +273,7 @@ cvc5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm) { return cmd.d_terms.front(); } - return cmd.d_nm->mkNode(Kind::PLUS, cmd.d_terms); + return cmd.d_nm->mkNode(Kind::ADD, cmd.d_terms); } poly::SignCondition normalize_kind(cvc5::Kind kind, diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 3992c31f6..918a81364 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -120,7 +120,7 @@ void ExponentialSolver::checkInitialRefine() Kind::OR, nm->mkNode(Kind::LEQ, t[0], d_data->d_zero), nm->mkNode( - Kind::GT, t, nm->mkNode(Kind::PLUS, t[0], d_data->d_one))); + Kind::GT, t, nm->mkNode(Kind::ADD, t[0], d_data->d_one))); CDProof* proof = nullptr; if (d_data->isProofEnabled()) { @@ -270,7 +270,7 @@ std::pair ExponentialSolver::getSecantBounds(TNode e, { // pick c+1 bounds.second = rewrite( - NodeManager::currentNM()->mkNode(Kind::PLUS, center, d_data->d_one)); + NodeManager::currentNM()->mkNode(Kind::ADD, center, d_data->d_one)); } return bounds; } diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index cbf867ef4..547bd3de3 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -47,7 +47,7 @@ Node mkBounds(TNode t, TNode lb, TNode ub) Node mkSecant(TNode t, TNode l, TNode u, TNode evall, TNode evalu) { NodeManager* nm = NodeManager::currentNM(); - return nm->mkNode(Kind::PLUS, + return nm->mkNode(Kind::ADD, evall, nm->mkNode(Kind::MULT, nm->mkNode(Kind::DIVISION, @@ -128,7 +128,7 @@ Node TranscendentalProofRuleChecker::checkInternal( Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]); return nm->mkNode(OR, nm->mkNode(LEQ, args[0], zero), - nm->mkNode(GT, e, nm->mkNode(PLUS, args[0], one))); + nm->mkNode(GT, e, nm->mkNode(ADD, args[0], one))); } else if (id == PfRule::ARITH_TRANS_EXP_ZERO) { @@ -232,10 +232,10 @@ Node TranscendentalProofRuleChecker::checkInternal( nm->mkNode(Kind::LEQ, x, pi), }), x.eqNode(y), - x.eqNode( - nm->mkNode(Kind::PLUS, - y, - nm->mkNode(Kind::MULT, nm->mkConstReal(2), s, pi)))), + x.eqNode(nm->mkNode( + Kind::ADD, + y, + nm->mkNode(Kind::MULT, nm->mkConstReal(2), s, pi)))), nm->mkNode(Kind::SINE, y).eqNode(nm->mkNode(Kind::SINE, x))}); } else if (id == PfRule::ARITH_TRANS_SINE_SYMMETRY) @@ -245,7 +245,7 @@ Node TranscendentalProofRuleChecker::checkInternal( Assert(args[0].getType().isReal()); Node s1 = nm->mkNode(Kind::SINE, args[0]); Node s2 = nm->mkNode(Kind::SINE, nm->mkNode(Kind::MULT, mone, args[0])); - return nm->mkNode(PLUS, s1, s2).eqNode(zero); + return nm->mkNode(ADD, s1, s2).eqNode(zero); } else if (id == PfRule::ARITH_TRANS_SINE_TANGENT_ZERO) { diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 3c5ae8006..d6a357b56 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -74,7 +74,7 @@ void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y) nm->mkNode(Kind::ITE, mkValidPhase(a[0], d_data->d_pi), a[0].eqNode(y), - a[0].eqNode(nm->mkNode(Kind::PLUS, + a[0].eqNode(nm->mkNode(Kind::ADD, y, nm->mkNode(Kind::MULT, nm->mkConstReal(Rational(2)), @@ -136,13 +136,13 @@ void SineSolver::checkInitialRefine() } { // sine symmetry: sin(t) - sin(-t) = 0 - Node lem = nm->mkNode(Kind::PLUS, t, symn).eqNode(d_data->d_zero); + Node lem = nm->mkNode(Kind::ADD, t, symn).eqNode(d_data->d_zero); CDProof* proof = nullptr; if (d_data->isProofEnabled()) { proof = d_data->getProof(); Node tmplem = - nm->mkNode(Kind::PLUS, + nm->mkNode(Kind::ADD, t, nm->mkNode( Kind::SINE, diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index 5afe3a705..f9ff63cc5 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -79,7 +79,7 @@ std::pair TaylorGenerator::getTaylor(Kind k, std::uint64_t n) factorial *= counter; varpow = nm->mkNode(Kind::MULT, d_taylor_real_fv, varpow); } - Node taylor_sum = (sum.size() == 1 ? sum[0] : nm->mkNode(Kind::PLUS, sum)); + Node taylor_sum = (sum.size() == 1 ? sum[0] : nm->mkNode(Kind::ADD, sum)); Node taylor_rem = nm->mkNode(Kind::DIVISION, varpow, nm->mkConstReal(factorial)); @@ -112,17 +112,17 @@ void TaylorGenerator::getPolynomialApproximationBounds( if (k == Kind::EXPONENTIAL) { pbounds.d_lower = taylor_sum; - pbounds.d_upperNeg = nm->mkNode(Kind::PLUS, taylor_sum, ru); + pbounds.d_upperNeg = nm->mkNode(Kind::ADD, taylor_sum, ru); pbounds.d_upperPos = nm->mkNode(Kind::MULT, taylor_sum, - nm->mkNode(Kind::PLUS, nm->mkConstReal(Rational(1)), ru)); + nm->mkNode(Kind::ADD, nm->mkConstReal(Rational(1)), ru)); } else { Assert(k == Kind::SINE); Node l = nm->mkNode(Kind::SUB, taylor_sum, ru); - Node u = nm->mkNode(Kind::PLUS, taylor_sum, ru); + Node u = nm->mkNode(Kind::ADD, taylor_sum, ru); pbounds.d_lower = l; pbounds.d_upperNeg = u; pbounds.d_upperPos = u; diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index fd5f7d07a..3ef9834e7 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -273,7 +273,7 @@ Node TranscendentalState::mkSecantPlane( Rational rcoeff = rcoeff_n.getConst(); Assert(rcoeff.sgn() != 0); Node res = - nm->mkNode(Kind::PLUS, + nm->mkNode(Kind::ADD, lval, nm->mkNode(Kind::MULT, nm->mkNode(Kind::DIVISION, diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index fe794ed72..3d2e0dc09 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -598,7 +598,8 @@ Node Polynomial::computeQR(const Polynomial& p, const Integer& div){ Polynomial p_q = Polynomial::mkPolynomial(q_vec); Polynomial p_r = Polynomial::mkPolynomial(r_vec); - return NodeManager::currentNM()->mkNode(kind::PLUS, p_q.getNode(), p_r.getNode()); + return NodeManager::currentNM()->mkNode( + kind::ADD, p_q.getNode(), p_r.getNode()); } @@ -633,7 +634,9 @@ bool Polynomial::variableMonomialAreStrictlyGreater(const Monomial& m) const{ bool Polynomial::isMember(TNode n) { if(Monomial::isMember(n)){ return true; - }else if(n.getKind() == kind::PLUS){ + } + else if (n.getKind() == kind::ADD) + { Assert(n.getNumChildren() >= 2); Node::iterator currIter = n.begin(), end = n.end(); Node prev = *currIter; @@ -655,7 +658,9 @@ bool Polynomial::isMember(TNode n) { mprev = mcurr; } return true; - } else { + } + else + { return false; } } @@ -669,7 +674,7 @@ Node SumPair::computeQR(const SumPair& sp, const Integer& div){ Integer::floorQR(constant_q, constant_r, constant, div); Node p_qr = Polynomial::computeQR(sp.getPolynomial(), div); - Assert(p_qr.getKind() == kind::PLUS); + Assert(p_qr.getKind() == kind::ADD); Assert(p_qr.getNumChildren() == 2); Polynomial p_q = Polynomial::parsePolynomial(p_qr[0]); @@ -678,7 +683,8 @@ Node SumPair::computeQR(const SumPair& sp, const Integer& div){ SumPair sp_q(p_q, Constant::mkConstant(constant_q)); SumPair sp_r(p_r, Constant::mkConstant(constant_r)); - return NodeManager::currentNM()->mkNode(kind::PLUS, sp_q.getNode(), sp_r.getNode()); + return NodeManager::currentNM()->mkNode( + kind::ADD, sp_q.getNode(), sp_r.getNode()); } SumPair SumPair::mkSumPair(const Polynomial& p){ diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index b96c51a9f..6ef32ea6e 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -800,7 +800,7 @@ private: static Node makePlusNode(const std::vector& m) { Assert(m.size() >= 2); - return makeNode(kind::PLUS, m.begin(), m.end()); + return makeNode(kind::ADD, m.begin(), m.end()); } typedef expr::NodeSelfIterator internal_iterator; @@ -932,7 +932,7 @@ public: if(singleton()){ return 1; }else{ - Assert(getNode().getKind() == kind::PLUS); + Assert(getNode().getKind() == kind::ADD); return getNode().getNumChildren(); } } @@ -1089,11 +1089,16 @@ public: } uint32_t numMonomials() const { - if( getNode().getKind() == kind::PLUS ){ + if (getNode().getKind() == kind::ADD) + { return getNode().getNumChildren(); - }else if(isZero()){ + } + else if (isZero()) + { return 0; - }else{ + } + else + { return 1; } } @@ -1147,7 +1152,8 @@ public: class SumPair : public NodeWrapper { private: static Node toNode(const Polynomial& p, const Constant& c){ - return NodeManager::currentNM()->mkNode(kind::PLUS, p.getNode(), c.getNode()); + return NodeManager::currentNM()->mkNode( + kind::ADD, p.getNode(), c.getNode()); } SumPair(TNode n) : NodeWrapper(n) { Assert(isNormalForm()); } @@ -1166,7 +1172,8 @@ private: } static bool isMember(TNode n) { - if(n.getKind() == kind::PLUS && n.getNumChildren() == 2){ + if (n.getKind() == kind::ADD && n.getNumChildren() == 2) + { if(Constant::isMember(n[1])){ if(Polynomial::isMember(n[0])){ Polynomial p = Polynomial::parsePolynomial(n[0]); @@ -1177,7 +1184,9 @@ private: }else{ return false; } - }else{ + } + else + { return false; } } diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index ab98f67ac..4d80bc495 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -170,10 +170,9 @@ Node OperatorElim::eliminateOperators(Node node, nm->mkNode( LT, num, - nm->mkNode( - MULT, - den, - nm->mkNode(PLUS, v, nm->mkConstInt(Rational(1)))))); + nm->mkNode(MULT, + den, + nm->mkNode(ADD, v, nm->mkConstInt(Rational(1)))))); } else { @@ -186,7 +185,7 @@ Node OperatorElim::eliminateOperators(Node node, nm->mkNode( MULT, den, - nm->mkNode(PLUS, v, nm->mkConstInt(Rational(-1)))))); + nm->mkNode(ADD, v, nm->mkConstInt(Rational(-1)))))); } } else @@ -206,8 +205,7 @@ Node OperatorElim::eliminateOperators(Node node, nm->mkNode( MULT, den, - nm->mkNode( - PLUS, v, nm->mkConstInt(Rational(1))))))), + nm->mkNode(ADD, v, nm->mkConstInt(Rational(1))))))), nm->mkNode( IMPLIES, nm->mkNode(LT, den, nm->mkConstInt(Rational(0))), @@ -221,7 +219,7 @@ Node OperatorElim::eliminateOperators(Node node, MULT, den, nm->mkNode( - PLUS, v, nm->mkConstInt(Rational(-1)))))))); + ADD, v, nm->mkConstInt(Rational(-1)))))))); } Node intVar = mkWitnessTerm( v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems); diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index c05f6ae0a..6e0494432 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -111,8 +111,8 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, // Whether a strict inequality is in the sum. bool strict = false; - NodeBuilder leftSum(Kind::PLUS); - NodeBuilder rightSum(Kind::PLUS); + NodeBuilder leftSum(Kind::ADD); + NodeBuilder rightSum(Kind::ADD); for (size_t i = 0; i < children.size(); ++i) { // Adjust strictness @@ -175,8 +175,8 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, // Whether a strict inequality is in the sum. bool strict = false; - NodeBuilder leftSum(Kind::PLUS); - NodeBuilder rightSum(Kind::PLUS); + NodeBuilder leftSum(Kind::ADD); + NodeBuilder rightSum(Kind::ADD); for (size_t i = 0; i < children.size(); ++i) { Rational scalar = args[i].getConst(); diff --git a/src/theory/arith/rewrites.h b/src/theory/arith/rewrites.h index 6053be916..996bc4520 100644 --- a/src/theory/arith/rewrites.h +++ b/src/theory/arith/rewrites.h @@ -50,7 +50,7 @@ enum class Rewrite : uint32_t // (mod (mod x c) c) --> (mod x c) MOD_OVER_MOD, // (mod (op ... (mod x c) ...) c) ---> (mod (op ... x ...) c) where - // op is one of { NONLINEAR_MULT, MULT, PLUS }. + // op is one of { NONLINEAR_MULT, MULT, ADD }. MOD_CHILD_MOD, // (div (mod x c) c) --> 0 DIV_OVER_MOD, diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 572af7fb3..6545ef923 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1155,7 +1155,8 @@ void TheoryArithPrivate::setupPolynomial(const Polynomial& poly) { } } - if(polyNode.getKind() == PLUS){ + if (polyNode.getKind() == ADD) + { d_tableauSizeHasBeenModified = true; vector variables; @@ -1193,7 +1194,7 @@ void TheoryArithPrivate::setupPolynomial(const Polynomial& poly) { /* Note: * It is worth documenting that polyNode should only be marked as - * being setup by this function if it has kind PLUS. + * being setup by this function if it has kind ADD. * Other kinds will be marked as being setup by lower levels of setup * specifically setupVariableList. */ @@ -1253,7 +1254,7 @@ void TheoryArithPrivate::releaseArithVar(ArithVar v){ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool aux, bool internal){ //TODO : The VarList trick is good enough? - Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS || internal); + Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == ADD || internal); if (logicInfo().isLinear() && Variable::isDivMember(x)) { stringstream ss; @@ -1690,7 +1691,7 @@ Node flattenAndSort(Node n){ switch(k){ case kind::OR: case kind::AND: - case kind::PLUS: + case kind::ADD: case kind::MULT: break; default: @@ -2076,7 +2077,7 @@ Node toSumNode(const ArithVariables& vars, const DenseMap& sum){ { return children[0]; } - return nm->mkNode(kind::PLUS, children); + return nm->mkNode(kind::ADD, children); } ConstraintCP TheoryArithPrivate::vectorToIntHoleConflict(const ConstraintCPVec& conflict){ @@ -3763,7 +3764,8 @@ DeltaRational TheoryArithPrivate::getDeltaValue(TNode term) const case kind::CONST_RATIONAL: return term.getConst(); - case kind::PLUS: { // 2+ args + case kind::ADD: + { // 2+ args DeltaRational value(0); for (TNode::iterator i = term.begin(), iend = term.end(); i != iend; ++i) { @@ -4958,7 +4960,10 @@ void TheoryArithPrivate::entailmentCheckBoundLookup(std::pair& tmp, int sgn, TNode tp) const { tmp.first = Node::null(); if(sgn == 0){ return; } - if(tp.getKind() != PLUS){ return; } + if (tp.getKind() != ADD) + { + return; + } Assert(Polynomial::isMember(tp)); tmp.second = DeltaRational(0); diff --git a/src/theory/bags/bag_reduction.cpp b/src/theory/bags/bag_reduction.cpp index 4e4b75c09..a4fba09b1 100644 --- a/src/theory/bags/bag_reduction.cpp +++ b/src/theory/bags/bag_reduction.cpp @@ -172,7 +172,7 @@ Node BagReduction::reduceCardOperator(Node node, std::vector& asserts) Node cardinality_0_equal = cardinality_0.eqNode(zero); Node uf_i_multiplicity = nm->mkNode(BAG_COUNT, uf_i, A); Node cardinality_i_equal = cardinality_i.eqNode( - nm->mkNode(PLUS, uf_i_multiplicity, cardinality_iMinusOne)); + nm->mkNode(ADD, uf_i_multiplicity, cardinality_iMinusOne)); Node unionDisjoint_0_equal = unionDisjoint_0.eqNode(nm->mkConst(EmptyBag(bagType))); Node bag = nm->mkBag(elementType, uf_i, uf_i_multiplicity); diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 24f313ad6..396e33557 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -458,7 +458,7 @@ BagsRewriteResponse BagsRewriter::rewriteCard(const TNode& n) const // (bag.card (bag.union-disjoint A B)) = (+ (bag.card A) (bag.card B)) Node A = d_nm->mkNode(BAG_CARD, n[0][0]); Node B = d_nm->mkNode(BAG_CARD, n[0][1]); - Node plus = d_nm->mkNode(PLUS, A, B); + Node plus = d_nm->mkNode(ADD, A, B); return BagsRewriteResponse(plus, Rewrite::CARD_DISJOINT); } return BagsRewriteResponse(n, Rewrite::NONE); diff --git a/src/theory/bags/card_solver.cpp b/src/theory/bags/card_solver.cpp index 2a35fb2bd..94c281c9a 100644 --- a/src/theory/bags/card_solver.cpp +++ b/src/theory/bags/card_solver.cpp @@ -411,7 +411,7 @@ void CardSolver::checkLeafBag(const std::pair& pair, counts.push_back(pairs[k].second); } counts.push_back(pairs[j].second); - Node sum = d_nm->mkNode(PLUS, counts); + Node sum = d_nm->mkNode(ADD, counts); Node premise; if (distinct.size() == 1) { diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 248f0337e..3cc2936fb 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -197,7 +197,7 @@ InferInfo InferenceGenerator::unionDisjoint(Node n, Node e) Node skolem = getSkolem(n, inferInfo); Node count = getMultiplicityTerm(e, skolem); - Node sum = d_nm->mkNode(PLUS, countA, countB); + Node sum = d_nm->mkNode(ADD, countA, countB); Node equal = count.eqNode(sum); inferInfo.d_conclusion = equal; @@ -367,7 +367,7 @@ InferInfo InferenceGenerator::cardUnionDisjoint(Node premise, lemmas.push_back(d_state->registerCardinalityTerm(card)); d_state->getCardinalitySkolem(card); Node skolem = d_state->getCardinalitySkolem(card); - sum = d_nm->mkNode(PLUS, sum, skolem); + sum = d_nm->mkNode(ADD, sum, skolem); ++it; } Node parentCard = d_nm->mkNode(BAG_CARD, parent); @@ -446,7 +446,7 @@ std::tuple InferenceGenerator::mapDownwards(Node n, bvm->mkBoundVar(n, "j", d_nm->integerType()); Node iList = d_nm->mkNode(BOUND_VAR_LIST, i); Node jList = d_nm->mkNode(BOUND_VAR_LIST, j); - Node iPlusOne = d_nm->mkNode(PLUS, i, d_one); + Node iPlusOne = d_nm->mkNode(ADD, i, d_one); Node iMinusOne = d_nm->mkNode(SUB, i, d_one); Node uf_i = d_nm->mkNode(APPLY_UF, uf, i); Node uf_j = d_nm->mkNode(APPLY_UF, uf, j); @@ -461,7 +461,7 @@ std::tuple InferenceGenerator::mapDownwards(Node n, Node count_iMinusOne = d_nm->mkNode(BAG_COUNT, uf_iMinusOne, A); Node count_uf_i = d_nm->mkNode(BAG_COUNT, uf_i, A); Node inductiveCase = - d_nm->mkNode(EQUAL, sum_i, d_nm->mkNode(PLUS, sum_iMinusOne, count_uf_i)); + d_nm->mkNode(EQUAL, sum_i, d_nm->mkNode(ADD, sum_iMinusOne, count_uf_i)); Node f_iEqualE = d_nm->mkNode(EQUAL, f_uf_i, e); Node geqOne = d_nm->mkNode(GEQ, count_uf_i, d_one); diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index f1a9ce70a..eb184174e 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -94,7 +94,7 @@ # upper bound, leave the colon after LB, but omit UB. For example, # an N-ary operator might be defined as: # -# operator PLUS 2: "addition on two or more arguments" +# operator ADD 2: "addition on two or more arguments" # # parameterized K1 K2 #children ["comment"] # diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index f69ca7854..875896cd4 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -448,7 +448,7 @@ Node IntBlaster::translateWithChildren( Node a = d_nm->mkNode(kind::MULT, translated_children[0], pow2BvSizeRight); Node b = translated_children[1]; - returnNode = d_nm->mkNode(kind::PLUS, a, b); + returnNode = d_nm->mkNode(kind::ADD, a, b); break; } case kind::BITVECTOR_EXTRACT: @@ -644,7 +644,7 @@ Node IntBlaster::createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount) Node thenResult = x; Node left = maxInt(amount); Node mul = d_nm->mkNode(kind::MULT, left, pow2(bvsize)); - Node sum = d_nm->mkNode(kind::PLUS, mul, x); + Node sum = d_nm->mkNode(kind::ADD, mul, x); Node elseResult = sum; Node ite = d_nm->mkNode(kind::ITE, condition, thenResult, elseResult); returnNode = ite; @@ -1071,7 +1071,7 @@ Node IntBlaster::createBVSubNode(Node x, Node y, uint64_t bvsize) Node IntBlaster::createBVAddNode(Node x, Node y, uint64_t bvsize) { - Node plus = d_nm->mkNode(kind::PLUS, x, y); + Node plus = d_nm->mkNode(kind::ADD, x, y); Node p2 = pow2(bvsize); return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, plus, p2); } diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index fd300fe41..2a040f75c 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -482,7 +482,7 @@ Node eliminateBv2Nat(TNode node) nm->mkNode(kind::ITE, cond, nm->mkConstInt(Rational(i)), z)); } // avoid plus with one child - return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children); + return children.size() == 1 ? children[0] : nm->mkNode(kind::ADD, children); } Node eliminateInt2Bv(TNode node) diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index a7a479550..82cca1083 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -81,7 +81,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) unsigned weight = c.getWeight(); children.push_back(nm->mkConstInt(Rational(weight))); Node res = - children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children); + children.size() == 1 ? children[0] : nm->mkNode(kind::ADD, children); Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite size " << in << " to " << res << std::endl; diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 2ec6dfe1b..03c1fe9e0 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -1380,7 +1380,7 @@ void SygusExtension::registerSizeTerm(Node e) Node mt = d_szinfo[m]->getOrMkActiveMeasureValue(); Node newMt = d_szinfo[m]->getOrMkActiveMeasureValue(true); Node ds = nm->mkNode(DT_SIZE, e); - slem = mt.eqNode(nm->mkNode(PLUS, newMt, ds)); + slem = mt.eqNode(nm->mkNode(ADD, newMt, ds)); } Trace("sygus-sb") << "...size lemma : " << slem << std::endl; d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_MT_BOUND); diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp index c819218ce..d17a21d4b 100644 --- a/src/theory/datatypes/sygus_simple_sym.cpp +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -38,13 +38,13 @@ SygusSimpleSymBreak::SygusSimpleSymBreak(quantifiers::TermDbSygus* tds) * * As a simple example, consider the trie: * root: - * d_req_kind = PLUS + * d_req_kind = ADD * d_children[0]: * d_req_type = A * d_children[1]: * d_req_type = A * This trie is satisfied by sygus types that have a constructor whose builtin - * kind is PLUS and whose argument types are both A. + * kind is ADD and whose argument types are both A. */ class ReqTrie { @@ -242,7 +242,7 @@ bool SygusSimpleSymBreak::considerArgKind( { // (not (~ x y)) -----> (~ (+ y 1) x) rt.d_req_kind = k; - rt.d_children[0].d_req_kind = PLUS; + rt.d_children[0].d_req_kind = ADD; rt.d_children[0].d_children[0].d_req_type = dt[c].getArgType(1); rt.d_children[0].d_children[1].d_req_const = NodeManager::currentNM()->mkConstInt(Rational(1)); @@ -253,7 +253,7 @@ bool SygusSimpleSymBreak::considerArgKind( // (not (~ x y)) -----> (~ y (+ x 1)) rt.d_req_kind = k; rt.d_children[0].d_req_type = dt[c].getArgType(1); - rt.d_children[1].d_req_kind = PLUS; + rt.d_children[1].d_req_kind = ADD; rt.d_children[1].d_children[0].d_req_type = dt[c].getArgType(0); rt.d_children[1].d_children[1].d_req_const = NodeManager::currentNM()->mkConstInt(Rational(1)); @@ -282,17 +282,17 @@ bool SygusSimpleSymBreak::considerArgKind( } else if (pk == NEG) { - if (k == PLUS) + if (k == ADD) { - rt.d_req_kind = PLUS; + rt.d_req_kind = ADD; reqk = NEG; } } else if (pk == BITVECTOR_NEG) { - if (k == PLUS) + if (k == ADD) { - rt.d_req_kind = PLUS; + rt.d_req_kind = ADD; reqk = BITVECTOR_NEG; } } @@ -337,15 +337,15 @@ bool SygusSimpleSymBreak::considerArgKind( // (~ (- y z) x) ----> (~ y (+ x z)) rt.d_req_kind = pk; rt.d_children[arg].d_req_type = dt[c].getArgType(0); - rt.d_children[oarg].d_req_kind = k == SUB ? PLUS : BITVECTOR_ADD; + rt.d_children[oarg].d_req_kind = k == SUB ? ADD : BITVECTOR_ADD; rt.d_children[oarg].d_children[0].d_req_type = pdt[pc].getArgType(oarg); rt.d_children[oarg].d_children[1].d_req_type = dt[c].getArgType(1); } - else if (pk == PLUS || pk == BITVECTOR_ADD) + else if (pk == ADD || pk == BITVECTOR_ADD) { // (+ x (- y z)) -----> (- (+ x y) z) // (+ (- y z) x) -----> (- (+ x y) z) - rt.d_req_kind = pk == PLUS ? SUB : BITVECTOR_SUB; + rt.d_req_kind = pk == ADD ? SUB : BITVECTOR_SUB; int oarg = arg == 0 ? 1 : 0; rt.d_children[0].d_req_kind = pk; rt.d_children[0].d_children[0].d_req_type = pdt[pc].getArgType(oarg); diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 1ab234ae9..461e9f4cc 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -416,7 +416,7 @@ EvalResult Evaluator::evalInternal( results[currNode] = EvalResult(av); break; } - case kind::PLUS: + case kind::ADD: { Rational res = results[currNode[0]].d_rat; for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 75db29207..277de7ae4 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -279,7 +279,7 @@ Node BvInverter::solveBvLit(Node sv, k = sv_t.getKind(); /* Note: All n-ary kinds except for CONCAT (i.e., BITVECTOR_AND, - * BITVECTOR_OR, MULT, PLUS) are commutative (no case split + * BITVECTOR_OR, MULT, ADD) are commutative (no case split * based on index). */ Node s = dropChild(sv_t, index); Assert((nchildren == 1 && s.isNull()) || (nchildren > 1 && !s.isNull())); diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 6528959c3..82a285f6f 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -183,7 +183,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, if (d_type.isInteger()) { uval = nm->mkNode( - PLUS, + ADD, val, nm->mkConstInt(Rational(isUpperBoundCTT(uires) ? 1 : -1))); uval = rewrite(uval); @@ -253,7 +253,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, { uires = is_upper ? CEG_TT_LOWER : CEG_TT_UPPER; uval = nm->mkNode( - PLUS, + ADD, val, nm->mkConstInt(Rational(isUpperBoundCTT(uires) ? 1 : -1))); uval = rewrite(uval); @@ -284,7 +284,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, } else { - vts_coeff_delta = nm->mkNode(PLUS, vts_coeff_delta, delta_coeff); + vts_coeff_delta = nm->mkNode(ADD, vts_coeff_delta, delta_coeff); vts_coeff_delta = rewrite(vts_coeff_delta); } } @@ -292,7 +292,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, { Node delta = d_vtc->getVtsDelta(); uval = - nm->mkNode(uires == CEG_TT_UPPER_STRICT ? PLUS : SUB, uval, delta); + nm->mkNode(uires == CEG_TT_UPPER_STRICT ? ADD : SUB, uval, delta); uval = rewrite(uval); } } @@ -609,7 +609,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, else { val = nm->mkNode(MULT, - nm->mkNode(PLUS, vals[0], vals[1]), + nm->mkNode(ADD, vals[0], vals[1]), nm->mkConstReal(Rational(1) / Rational(2))); val = rewrite(val); } @@ -618,7 +618,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { if (!vals[0].isNull()) { - val = nm->mkNode(PLUS, vals[0], d_one); + val = nm->mkNode(ADD, vals[0], d_one); val = rewrite(val); } else if (!vals[1].isNull()) @@ -754,7 +754,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable( && options().quantifiers.cegqiRoundUpLowerLia) { sf.d_subs[index] = nm->mkNode( - PLUS, + ADD, sf.d_subs[index], nm->mkNode( ITE, @@ -916,7 +916,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, Node realPart = real_part.empty() ? d_zero : (real_part.size() == 1 ? real_part[0] - : nm->mkNode(PLUS, real_part)); + : nm->mkNode(ADD, real_part)); Assert(ci->isEligibleForInstantiation(realPart)); // re-isolate Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl; @@ -933,8 +933,8 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, (msum[pv].isNull() || msum[pv].getConst().sgn() == 1) ? 1 : -1; val = rewrite( - nm->mkNode(ires_use == -1 ? PLUS : SUB, - nm->mkNode(ires_use == -1 ? SUB : PLUS, val, realPart), + nm->mkNode(ires_use == -1 ? ADD : SUB, + nm->mkNode(ires_use == -1 ? SUB : ADD, val, realPart), nm->mkNode(TO_INTEGER, realPart))); // could round up for upper bounds here Trace("cegqi-arith-debug") << "result : " << val << std::endl; @@ -1015,7 +1015,7 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta); rho = rewrite(rho); Trace("cegqi-arith-bound2") << rho << std::endl; - Kind rk = isLower ? PLUS : SUB; + Kind rk = isLower ? ADD : SUB; val = nm->mkNode(rk, val, rho); val = rewrite(val); Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl; @@ -1023,14 +1023,14 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, if (!inf_coeff.isNull()) { Assert(!d_vts_sym[0].isNull()); - val = nm->mkNode(PLUS, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0])); + val = nm->mkNode(ADD, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0])); val = rewrite(val); } if (!delta_coeff.isNull()) { // create delta here if necessary val = nm->mkNode( - PLUS, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta())); + ADD, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta())); val = rewrite(val); } return val; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index bd3f616d6..051d457ea 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -252,7 +252,7 @@ bool CegInstantiator::isEligible( Node n ) { CegHandledStatus CegInstantiator::isCbqiKind(Kind k) { - if (quantifiers::TermUtil::isBoolConnective(k) || k == PLUS || k == GEQ + if (quantifiers::TermUtil::isBoolConnective(k) || k == ADD || k == GEQ || k == EQUAL || k == MULT || k == NONLINEAR_MULT || k == DIVISION || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == TO_INTEGER @@ -1225,7 +1225,9 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node children.push_back( c ); Trace("sygus-si-apply-subs-debug") << "Add child : " << c << std::endl; } - Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); + Node nretc = children.size() == 1 + ? children[0] + : NodeManager::currentNM()->mkNode(ADD, children); nretc = rewrite(nretc); //ensure that nret does not contain vars if (!expr::hasSubterm(nretc, vars)) diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index fe852a90c..51a36518b 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -382,13 +382,13 @@ int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m) else { Assert(tn.isRealOrInt()); - t_match = nm->mkNode(PLUS, t, nm->mkConstRealOrInt(tn, Rational(1))); + t_match = nm->mkNode(ADD, t, nm->mkConstRealOrInt(tn, Rational(1))); } } else if (pat.getKind() == GEQ) { t_match = - nm->mkNode(PLUS, t, nm->mkConstRealOrInt(t.getType(), Rational(1))); + nm->mkNode(ADD, t, nm->mkConstRealOrInt(t.getType(), Rational(1))); } else if (pat.getKind() == GT) { diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index e792faa5f..77ab46868 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -613,7 +613,7 @@ Node PatternTermSelector::getInversionVariable(Node n) { return n; } - else if (nk == PLUS || nk == MULT) + else if (nk == ADD || nk == MULT) { Node ret; for (const Node& nc : n) @@ -659,7 +659,7 @@ Node PatternTermSelector::getInversion(Node n, Node x) { return x; } - else if (nk == PLUS || nk == MULT) + else if (nk == ADD || nk == MULT) { NodeManager* nm = NodeManager::currentNM(); int cindex = -1; @@ -669,7 +669,7 @@ Node PatternTermSelector::getInversion(Node n, Node x) Node nc = n[i]; if (!quantifiers::TermUtil::hasInstConstAttr(nc)) { - if (nk == PLUS) + if (nk == ADD) { x = nm->mkNode(SUB, x, nc); } diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp index 6ec3334cd..8c467489d 100644 --- a/src/theory/quantifiers/ematching/relational_match_generator.cpp +++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp @@ -95,7 +95,7 @@ int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m) if (!checkPol) { s = nm->mkNode( - PLUS, + ADD, s, nm->mkConstRealOrInt(s.getType(), Rational(d_rel == GEQ ? -1 : 1))); } diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 54fa24c76..2b44d2404 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -240,9 +240,9 @@ void BoundedIntegers::process( Node q, Node n, bool pol, n1 = veq[1]; n2 = veq[0]; if( n1.getKind()==BOUND_VARIABLE ){ - n2 = nm->mkNode(PLUS, n2, nm->mkConstInt(Rational(1))); + n2 = nm->mkNode(ADD, n2, nm->mkConstInt(Rational(1))); }else{ - n1 = nm->mkNode(PLUS, n1, nm->mkConstInt(Rational(-1))); + n1 = nm->mkNode(ADD, n1, nm->mkConstInt(Rational(-1))); } veq = nm->mkNode(GEQ, n1, n2); } @@ -829,7 +829,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; for (long k = 0; k < rr; k++) { - Node t = nm->mkNode(PLUS, tl, nm->mkConstInt(Rational(k))); + Node t = nm->mkNode(ADD, tl, nm->mkConstInt(Rational(k))); t = rewrite(t); elements.push_back( t ); } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index f87b1ab2c..082f24514 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -780,7 +780,8 @@ bool QuantInfo::completeMatch(std::vector& assigned, bool doContinue) slv_v = index; } Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl; - if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){ + if (d_vars[index].getKind() == ADD || d_vars[index].getKind() == MULT) + { Kind k = d_vars[index].getKind(); std::vector< TNode > children; for (const Node& vi : d_vars[index]){ @@ -835,7 +836,8 @@ bool QuantInfo::completeMatch(std::vector& assigned, bool doContinue) if (d_parent->atConflictEffort()) { Kind kn = k; - if( d_vars[index].getKind()==PLUS ){ + if (d_vars[index].getKind() == ADD) + { kn = SUB; } if( kn!=k ){ @@ -2546,7 +2548,8 @@ TNode QuantConflictFind::getZero(TypeNode tn, Kind k) if (it == d_zero.end()) { Node nn; - if( k==PLUS ){ + if (k == ADD) + { nn = NodeManager::currentNM()->mkConstRealOrInt(tn, Rational(0)); } d_zero[key] = nn; diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp index 9b9580b02..51b1a6d3c 100644 --- a/src/theory/quantifiers/quantifiers_macros.cpp +++ b/src/theory/quantifiers/quantifiers_macros.cpp @@ -194,7 +194,7 @@ void QuantifiersMacros::getMacroCandidates(Node n, candidates.push_back(n); } } - else if (n.getKind() == PLUS) + else if (n.getKind() == ADD) { for (size_t i = 0; i < n.getNumChildren(); i++) { diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index f1260eb69..479bbba1e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -928,11 +928,11 @@ Node QuantifiersRewriter::getVarElimEqString(Node lit, Node slvL = nm->mkNode(STRING_LENGTH, slv); Node tpreL = nm->mkNode(STRING_LENGTH, tpre); Node tpostL = nm->mkNode(STRING_LENGTH, tpost); - slv = nm->mkNode( - STRING_SUBSTR, - slv, - tpreL, - nm->mkNode(SUB, slvL, nm->mkNode(PLUS, tpreL, tpostL))); + slv = + nm->mkNode(STRING_SUBSTR, + slv, + tpreL, + nm->mkNode(SUB, slvL, nm->mkNode(ADD, tpreL, tpostL))); // forall x. r ++ x ++ t = s => P( x ) // is equivalent to // r ++ s' ++ t = s => P( s' ) where diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index f0684f04a..5530b8076 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -408,12 +408,12 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No if( n.getKind()==EQUAL ){ for( unsigned i=0; i<2; i++ ){ Node roff = nm->mkNode( - PLUS, r_add, nm->mkConstInt(Rational(i == 0 ? 1 : -1))); + ADD, r_add, nm->mkConstInt(Rational(i == 0 ? 1 : -1))); rdl.d_val.push_back(roff); } }else if( n.getKind()==GEQ ){ - Node roff = nm->mkNode( - PLUS, r_add, nm->mkConstInt(Rational(varLhs ? 1 : -1))); + Node roff = + nm->mkNode(ADD, r_add, nm->mkConstInt(Rational(varLhs ? 1 : -1))); rdl.d_val.push_back(roff); } } diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index c9706b40f..69d3b9f7a 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -485,7 +485,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) std::vector cargsPlus; cargsPlus.push_back(u); cargsPlus.push_back(u); - sdt.addConstructor(PLUS, cargsPlus); + sdt.addConstructor(ADD, cargsPlus); sdt.initializeDatatype(nm->integerType(), bvl, false, false); std::vector datatypes; datatypes.push_back(sdt.getDatatype()); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index dc7b3d5e9..c2a589565 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -773,8 +773,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( if (types[i].isRealOrInt()) { - // Add PLUS, SUB - Kind kinds[2] = {PLUS, SUB}; + // Add ADD, SUB + Kind kinds[2] = {ADD, SUB}; for (const Kind kind : kinds) { Trace("sygus-grammar-def") << "...add for " << kind << std::endl; @@ -802,9 +802,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector cargsEmpty; sdts.back().addConstructor( nm->mkConstInt(Rational(1)), "1", cargsEmpty); - /* Add operator PLUS */ - Kind kind = PLUS; - Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n"; + /* Add operator ADD */ + Kind kind = ADD; + Trace("sygus-grammar-def") << "\t...add for ADD to Pos_Int\n"; std::vector cargsPlus; cargsPlus.push_back(unresPosInt); cargsPlus.push_back(unresPosInt); @@ -1267,7 +1267,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargsAnyTerm.push_back(unresAnyConst); // make the sygus operator lambda X. c1*t1 + ... + cn*tn + c Assert(sumChildren.size() > 1); - Node ops = nm->mkNode(PLUS, sumChildren); + Node ops = nm->mkNode(ADD, sumChildren); Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lambdaVars), ops); Trace("sygus-grammar-def") << "any term operator is " << op << std::endl; // make the any term datatype, add to back @@ -1288,7 +1288,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector cargsPlus; cargsPlus.push_back(unres_types[iat]); cargsPlus.push_back(unres_types[iat]); - sdts[iat].d_sdt.addConstructor(PLUS, cargsPlus); + sdts[iat].d_sdt.addConstructor(ADD, cargsPlus); } // add the ITE, regardless of sum-of-monomials vs polynomial std::vector cargsIte; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index a1a314418..ddd16e605 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -146,7 +146,7 @@ void SygusGrammarNorm::TransfDrop::buildType(SygusGrammarNorm* sygus_norm, bool SygusGrammarNorm::TransfChain::isChainable(TypeNode tn, Node op) { /* Checks whether operator occurs chainable for its type */ - if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS) + if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == ADD) { return true; } @@ -158,7 +158,7 @@ bool SygusGrammarNorm::TransfChain::isChainable(TypeNode tn, Node op) function should realize that it is chainable for integers */ bool SygusGrammarNorm::TransfChain::isId(TypeNode tn, Node op, Node n) { - if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS + if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == ADD && n == TermUtil::mkTypeValue(tn, 0)) { return true; @@ -230,9 +230,9 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm, std::vector ctypesp; ctypesp.push_back(t); ctypesp.push_back(to.d_unres_tn); - to.d_sdt.addConstructor(nm->operatorOf(PLUS), kindToString(PLUS), ctypesp); + to.d_sdt.addConstructor(nm->operatorOf(ADD), kindToString(ADD), ctypesp); Trace("sygus-grammar-normalize-chain") - << "\tAdding PLUS to " << to.d_unres_tn << " with arg types " + << "\tAdding ADD to " << to.d_unres_tn << " with arg types " << to.d_unres_tn << " and " << t << "\n"; } /* In the initial case if not all operators claimed always creates a next */ @@ -316,10 +316,10 @@ std::unique_ptr SygusGrammarNorm::inferTransf( { Assert(op_pos[i] < dt.getNumConstructors()); Node sop = dt[op_pos[i]].getSygusOp(); - /* Collects a chainable operator such as PLUS */ + /* Collects a chainable operator such as ADD */ if (sop.getKind() == BUILTIN && TransfChain::isChainable(sygus_tn, sop)) { - Assert(nm->operatorToKind(sop) == PLUS); + Assert(nm->operatorToKind(sop) == ADD); /* TODO #1304: be robust for this case */ /* For now only transforms applications whose arguments have the same type * as the root */ @@ -337,7 +337,7 @@ std::unique_ptr SygusGrammarNorm::inferTransf( if (!same_type_plus) { Trace("sygus-grammar-normalize-infer") - << "\tFor OP " << PLUS << " did not collecting sop " << sop + << "\tFor OP " << ADD << " did not collecting sop " << sop << " in position " << op_pos[i] << "\n"; continue; } @@ -349,8 +349,8 @@ std::unique_ptr SygusGrammarNorm::inferTransf( continue; } /* TODO #1304: check this for each operator */ - /* Collects elements that are not the identity (e.g. 0 is the id of PLUS) */ - if (!TransfChain::isId(sygus_tn, nm->operatorOf(PLUS), sop)) + /* Collects elements that are not the identity (e.g. 0 is the id of ADD) */ + if (!TransfChain::isId(sygus_tn, nm->operatorOf(ADD), sop)) { Trace("sygus-grammar-normalize-infer") << "\tCollecting for NON_ID_ELEMS the sop " << sop diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index cdaf97487..fd39323af 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -273,7 +273,7 @@ class SygusGrammarNorm : protected EnvObj * neutral element. * * TODO: #1304: - * - define this transformation for more than just PLUS for Int. + * - define this transformation for more than just ADD for Int. * - improve the building such that elements that should not be entitled a * "link in the chain" (such as 5 in opposition to variables and 1) do not get * one @@ -319,7 +319,7 @@ class SygusGrammarNorm : protected EnvObj const DType& dt, std::vector& op_pos) override; - /** Whether operator is chainable for the type (e.g. PLUS for Int) + /** Whether operator is chainable for the type (e.g. ADD for Int) * * Since the map this function depends on cannot be built statically, this * function first build maps the first time a type is checked. As a @@ -331,7 +331,7 @@ class SygusGrammarNorm : protected EnvObj */ static bool isChainable(TypeNode tn, Node op); /* Whether n is the identity for the chain operator of the type (e.g. 1 is - * not the identity 0 for PLUS for Int) + * not the identity 0 for ADD for Int) * * TODO: #1304: Cover more types, make this robust to more complex grammars */ @@ -354,7 +354,7 @@ class SygusGrammarNorm : protected EnvObj static std::map> d_chain_ops; /** Specifies for each type node and chainable operator its identity * - * For example, for Int and PLUS the map is {Int -> {+ -> 0}} + * For example, for Int and ADD the map is {Int -> {+ -> 0}} * * TODO #1304: consider more operators */ diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 7a8ff0b1d..a1f66d24d 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -163,7 +163,7 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn) Trace("sygus-db") << std::endl; // We must properly catch type errors in sygus grammars for arguments of // builtin operators. The challenge is that we easily ask for expected - // argument types of builtin operators e.g. PLUS. Hence we use a call to + // argument types of builtin operators e.g. ADD. Hence we use a call to // mkGeneric below. This ensures that terms that this constructor encodes // are of the type specified in the datatype. This will fail if // e.g. bitvector-and is a constructor of an integer grammar. Our (version diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 2d0561462..b2320481f 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -604,7 +604,7 @@ Node SygusSampler::getRandomValue(TypeNode tn) } else { - ret = nm->mkNode(kind::PLUS, sum); + ret = nm->mkNode(kind::ADD, sum); } if (Random::getRandom().pickWithProb(0.5)) diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 214b9ca96..3830c6237 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -130,27 +130,27 @@ class TermDb : public QuantifiersUtil { /** Get the currently added ground terms for the given operator */ DbList* getOrMkDbListForOp(TNode op); /** get match operator for term n - * - * If n has a kind that we index, this function will - * typically return n.getOperator(). - * - * However, for parametric operators f, the match operator is an arbitrary - * chosen f-application. For example, consider array select: - * A : (Array Int Int) - * B : (Array Bool Int) - * We require that terms like (select A 1) and (select B 2) are indexed in - * separate - * data structures despite the fact that - * (select A 1).getOperator()==(select B 2).getOperator(). - * Hence, for the above terms, we may return: - * getMatchOperator( (select A 1) ) = (select A 1), and - * getMatchOperator( (select B 2) ) = (select B 2). - * The match operator is the first instance of an application of the parametric - * operator of its type. - * - * If n has a kind that we do not index (like PLUS), - * then this function returns Node::null(). - */ + * + * If n has a kind that we index, this function will + * typically return n.getOperator(). + * + * However, for parametric operators f, the match operator is an arbitrary + * chosen f-application. For example, consider array select: + * A : (Array Int Int) + * B : (Array Bool Int) + * We require that terms like (select A 1) and (select B 2) are indexed in + * separate + * data structures despite the fact that + * (select A 1).getOperator()==(select B 2).getOperator(). + * Hence, for the above terms, we may return: + * getMatchOperator( (select A 1) ) = (select A 1), and + * getMatchOperator( (select B 2) ) = (select B 2). + * The match operator is the first instance of an application of the + * parametric operator of its type. + * + * If n has a kind that we do not index (like ADD), + * then this function returns Node::null(). + */ Node getMatchOperator(Node n); /** get term arg index for all f-applications in the current context */ TNodeTrie* getTermArgTrie(Node f); diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 23372b794..670b75c99 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -275,7 +275,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry) return false; } } - return k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR + return k == ADD || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT @@ -292,7 +292,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry) return false; } } - return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND + return k == EQUAL || k == ADD || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTER @@ -432,7 +432,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg) TypeNode tn = n.getType(); if (n == mkTypeValue(tn, 0)) { - if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_ADD + if (ik == ADD || ik == OR || ik == XOR || ik == BITVECTOR_ADD || ik == BITVECTOR_OR || ik == BITVECTOR_XOR || ik == STRING_CONCAT) { return true; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 9cf2a908d..cc642127c 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -284,7 +284,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { Node ret = NodeManager::currentNM()->mkNode( kind::SUB, NodeManager::currentNM()->mkNode( - kind::PLUS, + kind::ADD, NodeManager::currentNM()->mkNode(kind::SET_CARD, node[0][0]), NodeManager::currentNM()->mkNode(kind::SET_CARD, node[0][1])), NodeManager::currentNM()->mkNode( diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 46d89520b..eb9e07bdc 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -201,7 +201,7 @@ bool ArithEntail::checkApprox(Node ar) // get the current "fixed" sum for the abstraction of ar Node aar = aarSum.empty() ? d_zero - : (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(PLUS, aarSum)); + : (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(ADD, aarSum)); aar = d_rr->rewrite(aar); Trace("strings-ent-approx-debug") << "...processed fixed sum " << aar << " with " << mApprox.size() @@ -328,7 +328,7 @@ bool ArithEntail::checkApprox(Node ar) Assert(!v.isNull() && !vapprox.isNull()); Assert(msum.find(v) != msum.end()); Node mn = ArithMSum::mkCoeffTerm(msum[v], vapprox); - aar = nm->mkNode(PLUS, aar, mn); + aar = nm->mkNode(ADD, aar, mn); // update the msumAar map aar = d_rr->rewrite(aar); msumAar.clear(); @@ -377,9 +377,9 @@ void ArithEntail::getArithApproximations(Node a, bool isOverApprox) { NodeManager* nm = NodeManager::currentNM(); - // We do not handle PLUS here since this leads to exponential behavior. + // We do not handle ADD here since this leads to exponential behavior. // Instead, this is managed, e.g. during checkApprox, where - // PLUS terms are expanded "on-demand" during the reasoning. + // ADD terms are expanded "on-demand" during the reasoning. Trace("strings-ent-approx-debug") << "Get arith approximations " << a << std::endl; Kind ak = a.getKind(); @@ -428,7 +428,7 @@ void ArithEntail::getArithApproximations(Node a, { // 0 <= n and n+m <= len( x ) implies // m <= len( substr( x, n, m ) ) - Node npm = nm->mkNode(PLUS, a[0][1], a[0][2]); + Node npm = nm->mkNode(ADD, a[0][1], a[0][2]); if (check(a[0][1]) && check(lenx, npm)) { approx.push_back(a[0][2]); @@ -459,7 +459,7 @@ void ArithEntail::getArithApproximations(Node a, else { // len( x ) + len( z ) >= len( replace( x, y, z ) ) - approx.push_back(nm->mkNode(PLUS, lenx, lenz)); + approx.push_back(nm->mkNode(ADD, lenx, lenz)); } } else @@ -495,7 +495,7 @@ void ArithEntail::getArithApproximations(Node a, // x >= 0 implies // x+1 >= len( int.to.str( x ) ) approx.push_back( - nm->mkNode(PLUS, nm->mkConstInt(Rational(1)), a[0][0])); + nm->mkNode(ADD, nm->mkConstInt(Rational(1)), a[0][0])); } } } @@ -575,7 +575,7 @@ bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict) Node curr = toVisit.back(); toVisit.pop_back(); - if (curr.getKind() == kind::PLUS || curr.getKind() == kind::MULT + if (curr.getKind() == kind::ADD || curr.getKind() == kind::MULT || curr.getKind() == kind::SUB || curr.getKind() == kind::EQUAL) { for (const auto& currChild : curr) @@ -666,7 +666,7 @@ bool ArithEntail::checkWithAssumption(Node assumption, Node s = nm->mkBoundVar("slackVal", nm->stringType()); Node slen = nm->mkNode(kind::STRING_LENGTH, s); assumption = d_rr->rewrite( - nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::PLUS, y, slen))); + nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::ADD, y, slen))); } Node diff = nm->mkNode(kind::SUB, a, b); @@ -780,7 +780,7 @@ Node ArithEntail::getConstantBound(TNode a, bool isLower) ret = d_zero; } } - else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT) + else if (a.getKind() == kind::ADD || a.getKind() == kind::MULT) { std::vector children; bool success = true; @@ -916,7 +916,7 @@ bool ArithEntail::checkInternal(Node a) // str.len( t ) >= 0 return true; } - else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT) + else if (a.getKind() == kind::ADD || a.getKind() == kind::MULT) { for (unsigned i = 0; i < a.getNumChildren(); i++) { @@ -941,7 +941,7 @@ bool ArithEntail::inferZerosInSumGeq(Node x, NodeManager* nm = NodeManager::currentNM(); // Check if we can show that y1 + ... + yn >= x - Node sum = (ys.size() > 1) ? nm->mkNode(PLUS, ys) : ys[0]; + Node sum = (ys.size() > 1) ? nm->mkNode(ADD, ys) : ys[0]; if (!check(sum, x)) { return false; @@ -960,7 +960,7 @@ bool ArithEntail::inferZerosInSumGeq(Node x, std::vector::iterator pos = ys.erase(ys.begin() + i); if (ys.size() > 1) { - sum = nm->mkNode(PLUS, ys); + sum = nm->mkNode(ADD, ys); } else { diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp index 58d1efaf7..98777c4bd 100644 --- a/src/theory/strings/array_core_solver.cpp +++ b/src/theory/strings/array_core_solver.cpp @@ -237,7 +237,7 @@ void ArrayCoreSolver::check(const std::vector& nthTerms, Node i = n[1]; Node sLen = nm->mkNode(STRING_LENGTH, s); Node iRev = nm->mkNode( - SUB, sLen, nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1)))); + SUB, sLen, nm->mkNode(ADD, i, nm->mkConstInt(Rational(1)))); std::vector nexp; nexp.push_back(nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), i)); diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp index d7663170a..89dadd695 100644 --- a/src/theory/strings/array_solver.cpp +++ b/src/theory/strings/array_solver.cpp @@ -266,7 +266,7 @@ void ArraySolver::checkTerm(Node t, bool checkInv) Node currSum = d_zero; if (!lacc.empty()) { - currSum = lacc.size() == 1 ? lacc[0] : nm->mkNode(PLUS, lacc); + currSum = lacc.size() == 1 ? lacc[0] : nm->mkNode(ADD, lacc); currIndex = nm->mkNode(SUB, currIndex, currSum); } Node cc; @@ -316,7 +316,7 @@ void ArraySolver::checkTerm(Node t, bool checkInv) lacc.push_back(clen); if (k == SEQ_NTH) { - Node currSumPost = lacc.size() == 1 ? lacc[0] : nm->mkNode(PLUS, lacc); + Node currSumPost = lacc.size() == 1 ? lacc[0] : nm->mkNode(ADD, lacc); Node cf = nm->mkNode(LT, t[1], currSumPost); Trace("seq-array-debug") << "......condition " << cf << std::endl; cond.push_back(cf); diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index a94f09cb7..d1de218c9 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -144,7 +144,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) } } Node lenSum = childLengths.size() > 1 - ? nm->mkNode(PLUS, childLengths) + ? nm->mkNode(ADD, childLengths) : (childLengths.empty() ? zero : childLengths[0]); // if we have a fixed length if (hasFixedLength) @@ -159,7 +159,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) { Node ppSum = childLengthsPostPivot.size() == 1 ? childLengthsPostPivot[0] - : nm->mkNode(PLUS, childLengthsPostPivot); + : nm->mkNode(ADD, childLengthsPostPivot); currEnd = nm->mkNode(SUB, lenx, ppSum); } else @@ -173,7 +173,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node currMem = nm->mkNode(STRING_IN_REGEXP, curr, re[i]); conc.push_back(currMem); } - currEnd = nm->mkNode(PLUS, currEnd, childLengths[i]); + currEnd = nm->mkNode(ADD, currEnd, childLengths[i]); } } Node res = nm->mkNode(AND, conc); @@ -252,8 +252,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) if (gap_minsize[i] > 0) { // the gap to this child is at least gap_minsize[i] - prev_end = nm->mkNode( - PLUS, prev_end, nm->mkConstInt(Rational(gap_minsize[i]))); + prev_end = + nm->mkNode(ADD, prev_end, nm->mkConstInt(Rational(gap_minsize[i]))); } prev_ends.push_back(prev_end); Node sc = sep_children[i]; @@ -264,7 +264,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node curr = prev_end; Node ss = nm->mkNode(STRING_SUBSTR, x, curr, lensc); conj.push_back(ss.eqNode(sc)); - prev_end = nm->mkNode(PLUS, curr, lensc); + prev_end = nm->mkNode(ADD, curr, lensc); } else { @@ -284,12 +284,12 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node k = bvm->mkBoundVar(cacheVal, intType); non_greedy_find_vars.push_back(k); - prev_end = nm->mkNode(PLUS, prev_end, k); + prev_end = nm->mkNode(ADD, prev_end, k); } Node curr = nm->mkNode(STRING_INDEXOF, x, sc, prev_end); Node idofFind = curr.eqNode(nm->mkConstInt(Rational(-1))).negate(); conj.push_back(idofFind); - prev_end = nm->mkNode(PLUS, curr, lensc); + prev_end = nm->mkNode(ADD, curr, lensc); } } @@ -312,7 +312,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) // ... ^ "B" = substr( x, len( x ) - 3, 1 ) ^ ... Node sc = sep_children.back(); Node lenSc = nm->mkNode(STRING_LENGTH, sc); - Node loc = nm->mkNode(SUB, lenx, nm->mkNode(PLUS, lenSc, cEnd)); + Node loc = nm->mkNode(SUB, lenx, nm->mkNode(ADD, lenSc, cEnd)); Node scc = sc.eqNode(nm->mkNode(STRING_SUBSTR, x, loc, lenSc)); // We also must ensure that we fit. This constraint is necessary in // addition to the constraint above. Take this example: @@ -352,7 +352,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) // For example: // x in (re.++ "A" (re.* _) "B" _ _ (re.* _)) ---> // ... ^ indexof( x, "B", 1 ) + 2 <= len( x ) - Node fit = nm->mkNode(LEQ, nm->mkNode(PLUS, prev_end, cEnd), lenx); + Node fit = nm->mkNode(LEQ, nm->mkNode(ADD, prev_end, cEnd), lenx); conj.push_back(fit); } Node res = nm->mkAnd(conj); @@ -500,7 +500,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) std::vector rsuffix; rsuffix.insert(rsuffix.end(), children.begin() + i + 1, children.end()); Node rps = utils::mkConcat(rsuffix, nm->regExpType()); - Node ks = nm->mkNode(PLUS, k, lens); + Node ks = nm->mkNode(ADD, k, lens); Node substrSuffix = nm->mkNode( STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, x, ks, nm->mkNode(SUB, lenx, ks)), diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 3068c6815..99978b015 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -616,7 +616,7 @@ Node SequencesRewriter::rewriteLength(Node node) kind::STRING_LENGTH, tmpNode[i])); } } - Node retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec); + Node retNode = NodeManager::currentNM()->mkNode(kind::ADD, node_vec); return returnRewrite(node, retNode, Rewrite::LEN_CONCAT); } } @@ -1977,7 +1977,7 @@ Node SequencesRewriter::rewriteSubstr(Node node) Node tot_len = d_arithEntail.rewrite(nm->mkNode(kind::STRING_LENGTH, node[0])); Node end_pt = - d_arithEntail.rewrite(nm->mkNode(kind::PLUS, node[1], node[2])); + d_arithEntail.rewrite(nm->mkNode(kind::ADD, node[1], node[2])); if (node[2] != tot_len) { if (d_arithEntail.check(node[2], tot_len)) @@ -2049,7 +2049,7 @@ Node SequencesRewriter::rewriteSubstr(Node node) } if (!new_len.isNull()) { - Node new_start = nm->mkNode(kind::PLUS, start_inner, start_outer); + Node new_start = nm->mkNode(kind::ADD, start_inner, start_outer); Node ret = nm->mkNode(kind::STRING_SUBSTR, node[0][0], new_start, new_len); return returnRewrite(node, ret, Rewrite::SS_COMBINE); @@ -2137,7 +2137,7 @@ Node SequencesRewriter::rewriteUpdate(Node node) // str.rev(str.update(s, len(s) - (n + 1), t)) Node idx = nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, s), - nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1)))); + nm->mkNode(ADD, i, nm->mkConstInt(Rational(1)))); Node ret = nm->mkNode(STRING_REV, nm->mkNode(STRING_UPDATE, s[0], idx, x)); return returnRewrite(node, ret, Rewrite::UPD_REV); } @@ -2639,7 +2639,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) // str.indexof(str.++("AB", x, "C"), "C", 0) ---> // 2 + str.indexof(str.++(x, "C"), "C", 0) Node ret = nm->mkNode( - kind::PLUS, + kind::ADD, nm->mkNode(kind::STRING_LENGTH, utils::mkConcat(nb, stype)), nm->mkNode(kind::STRING_INDEXOF, utils::mkConcat(children0, stype), @@ -2667,7 +2667,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) ) Node nn = utils::mkConcat(children0, stype); Node ret = - nm->mkNode(PLUS, + nm->mkNode(ADD, nm->mkNode(SUB, node[2], new_len), nm->mkNode(STRING_INDEXOF, nn, node[1], new_len)); return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN); @@ -3021,12 +3021,12 @@ Node SequencesRewriter::rewriteReplace(Node node) // Length of the non-substr components in the second argument Node partLen1 = nm->mkNode(kind::STRING_LENGTH, utils::mkConcat(children1, stype)); - Node maxLen1 = nm->mkNode(kind::PLUS, partLen1, lastChild1[2]); + Node maxLen1 = nm->mkNode(kind::ADD, partLen1, lastChild1[2]); Node zero = nm->mkConstInt(Rational(0)); Node one = nm->mkConstInt(Rational(1)); Node len0 = nm->mkNode(kind::STRING_LENGTH, node[0]); - Node len0_1 = nm->mkNode(kind::PLUS, len0, one); + Node len0_1 = nm->mkNode(kind::ADD, len0, one); // Check len(t) + j > len(x) + 1 if (d_arithEntail.check(maxLen1, len0_1, true)) { @@ -3034,7 +3034,7 @@ Node SequencesRewriter::rewriteReplace(Node node) kind::STRING_SUBSTR, lastChild1[0], lastChild1[1], - nm->mkNode(kind::PLUS, len0, one, nm->mkNode(kind::NEG, partLen1)))); + nm->mkNode(kind::ADD, len0, one, nm->mkNode(kind::NEG, partLen1)))); Node res = nm->mkNode(kind::STRING_REPLACE, node[0], utils::mkConcat(children1, stype), @@ -3595,7 +3595,7 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype) // sorts do not permit values that the solver can handle (e.g. uninterpreted // sorts and arrays). } - else if (len.getKind() == PLUS) + else if (len.getKind() == ADD) { // x + y -> norm(x) + norm(y) NodeBuilder concatBuilder(STRING_CONCAT); diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index a92fd3424..c81059712 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -198,7 +198,7 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) id = SK_SUFFIX_REM; Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre"); b = nm->mkNode( - PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b)); + ADD, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b)); } else if (id == SK_ID_V_SPT || id == SK_ID_C_SPT) { diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index 7491f510f..90a5446a1 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -429,7 +429,7 @@ bool StringsEntail::componentContainsBase( { bool success = true; Node start_pos = n2[1]; - Node end_pos = nm->mkNode(PLUS, n2[1], n2[2]); + Node end_pos = nm->mkNode(ADD, n2[1], n2[2]); Node len_n2s = nm->mkNode(STRING_LENGTH, n2[0]); if (dir == 1) { diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp index a3ae03099..dfc179614 100644 --- a/src/theory/strings/strings_fmf.cpp +++ b/src/theory/strings/strings_fmf.cpp @@ -73,7 +73,7 @@ void StringsFmf::StringSumLengthDecisionStrategy::initialize( { sum.push_back(nm->mkNode(STRING_LENGTH, v)); } - Node sumn = sum.size() == 1 ? sum[0] : nm->mkNode(PLUS, sum); + Node sumn = sum.size() == 1 ? sum[0] : nm->mkNode(ADD, sum); d_inputVarLsum.set(sumn); } } diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 85ec680ac..d648a9287 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -410,7 +410,7 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n) nodeVec.push_back(lni); } } - lsum = nm->mkNode(PLUS, nodeVec); + lsum = nm->mkNode(ADD, nodeVec); lsum = rewrite(lsum); } else if (n.isConst()) diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 2667c1989..97dbd2b3f 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -63,7 +63,7 @@ Node StringsPreprocess::reduce(Node t, Node n = t[1]; Node m = t[2]; Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst"); - Node t12 = nm->mkNode(PLUS, n, m); + Node t12 = nm->mkNode(ADD, n, m); Node lt0 = nm->mkNode(STRING_LENGTH, s); //start point is greater than or equal zero Node c1 = nm->mkNode(GEQ, n, zero); @@ -85,7 +85,7 @@ Node StringsPreprocess::reduce(Node t, // len(s) - n -m Node b13 = nm->mkNode( OR, - nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, nm->mkNode(PLUS, n, m))), + nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, nm->mkNode(ADD, n, m))), nm->mkNode(EQUAL, lsk2, zero)); // Length of the result is at most m Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m); @@ -142,7 +142,7 @@ Node StringsPreprocess::reduce(Node t, rs = nm->mkNode(STRING_SUBSTR, r, zero, nm->mkNode(SUB, lens, n)); } Node rslen = nm->mkNode(STRING_LENGTH, rs); - Node nsuf = nm->mkNode(PLUS, n, rslen); + Node nsuf = nm->mkNode(ADD, n, rslen); // substr(s, n, len(substr(r,0,|s|-n))), which is used for formalizing the // purification variable sk3 below. Node ssubstr = nm->mkNode(STRING_SUBSTR, s, n, rslen); @@ -226,7 +226,7 @@ Node StringsPreprocess::reduce(Node t, y) .negate(); // skk = n + len( io2 ) - Node c33 = skk.eqNode(nm->mkNode(PLUS, n, nm->mkNode(STRING_LENGTH, io2))); + Node c33 = skk.eqNode(nm->mkNode(ADD, n, nm->mkNode(STRING_LENGTH, io2))); Node cc3 = nm->mkNode(AND, c31, c32, c33); // assert: @@ -351,7 +351,7 @@ Node StringsPreprocess::reduce(Node t, conc.push_back(lem); Node x = SkolemCache::mkIndexVar(t); - Node xPlusOne = nm->mkNode(PLUS, x, one); + Node xPlusOne = nm->mkNode(ADD, x, one); Node xbv = nm->mkNode(BOUND_VAR_LIST, x); Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, leni)); Node sx = nm->mkNode(STRING_SUBSTR, itost, x, one); @@ -361,7 +361,7 @@ Node StringsPreprocess::reduce(Node t, Node c = nm->mkNode(SUB, nm->mkNode(STRING_TO_CODE, sx), c0); Node ten = nm->mkConstInt(Rational(10)); - Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux))); + Node eq = ux1.eqNode(nm->mkNode(ADD, c, nm->mkNode(MULT, ten, ux))); Node leadingZeroPos = nm->mkNode(AND, x.eqNode(zero), nm->mkNode(GT, leni, one)); Node cb = nm->mkNode( @@ -453,10 +453,10 @@ Node StringsPreprocess::reduce(Node t, Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, lens)); Node sx = nm->mkNode(STRING_SUBSTR, s, x, one); Node ux = nm->mkNode(APPLY_UF, u, x); - Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, one)); + Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(ADD, x, one)); Node c = nm->mkNode(SUB, nm->mkNode(STRING_TO_CODE, sx), c0); - Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux))); + Node eq = ux1.eqNode(nm->mkNode(ADD, c, nm->mkNode(MULT, ten, ux))); Node cb = nm->mkNode(AND, nm->mkNode(GEQ, c, zero), nm->mkNode(LT, c, ten)); Node ux1lem = nm->mkNode(GEQ, stoit, ux1); @@ -497,7 +497,7 @@ Node StringsPreprocess::reduce(Node t, Node s = t[0]; Node n = t[1]; Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst"); - Node t12 = nm->mkNode(PLUS, n, one); + Node t12 = nm->mkNode(ADD, n, one); Node lt0 = nm->mkNode(STRING_LENGTH, s); // start point is greater than or equal zero Node c1 = nm->mkNode(GEQ, n, zero); @@ -628,19 +628,19 @@ Node StringsPreprocess::reduce(Node t, Node bound = nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc)); Node ufi = nm->mkNode(APPLY_UF, uf, i); - Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, one)); + Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(ADD, i, one)); Node ii = nm->mkNode(STRING_INDEXOF, x, y, ufi); Node cc = nm->mkNode(STRING_CONCAT, nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(SUB, ii, ufi)), z, - nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one))); + nm->mkNode(APPLY_UF, us, nm->mkNode(ADD, i, one))); std::vector flem; flem.push_back(ii.eqNode(negOne).negate()); flem.push_back(nm->mkNode(APPLY_UF, us, i).eqNode(cc)); flem.push_back( - ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y)))); + ufip1.eqNode(nm->mkNode(ADD, ii, nm->mkNode(STRING_LENGTH, y)))); Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem)); Node q = utils::mkForallInternal(bvli, body); @@ -773,7 +773,7 @@ Node StringsPreprocess::reduce(Node t, Node bvli = nm->mkNode(BOUND_VAR_LIST, i); Node bound = nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc)); - Node ip1 = nm->mkNode(PLUS, i, one); + Node ip1 = nm->mkNode(ADD, i, one); Node ufi = nm->mkNode(APPLY_UF, uf, i); Node ufip1 = nm->mkNode(APPLY_UF, uf, ip1); Node ulip1 = nm->mkNode(APPLY_UF, ul, ip1); @@ -785,7 +785,7 @@ Node StringsPreprocess::reduce(Node t, flem.push_back(nm->mkNode(GT, ulip1, zero)); // Uf(i + 1) = indexof_re(x, yp, Uf(i)) + Ul(i + 1) flem.push_back(ufip1.eqNode( - nm->mkNode(PLUS, nm->mkNode(STRING_INDEXOF_RE, x, yp, ufi), ulip1))); + nm->mkNode(ADD, nm->mkNode(STRING_INDEXOF_RE, x, yp, ufi), ulip1))); // in_re(substr(x, ii, Ul(i + 1)), y') flem.push_back(nm->mkNode( STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, x, ii, ulip1), yp)); @@ -869,7 +869,7 @@ Node StringsPreprocess::reduce(Node t, Node res = nm->mkNode( ITE, nm->mkNode(AND, nm->mkNode(LEQ, lb, ci), nm->mkNode(LEQ, ci, ub)), - nm->mkNode(PLUS, ci, offset), + nm->mkNode(ADD, ci, offset), ci); Node bound = @@ -903,7 +903,7 @@ Node StringsPreprocess::reduce(Node t, Node bvi = nm->mkNode(BOUND_VAR_LIST, i); Node revi = - nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one)); + nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), nm->mkNode(ADD, i, one)); Node ssr = nm->mkNode(STRING_SUBSTR, r, i, one); Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, one); diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index c1f7c880f..ada7619e2 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -221,7 +221,7 @@ class TheoryModel : protected EnvObj * kind k in getModelValue. We distinguish four categories of kinds: * * [1] "Evaluated" - * This includes (standard) interpreted symbols like NOT, PLUS, SET_UNION, + * This includes (standard) interpreted symbols like NOT, ADD, SET_UNION, * etc. These operators can be characterized by the invariant that they are * "evaluatable". That is, if they are applied to only constants, the rewriter * is guaranteed to rewrite the application to a constant. When getting diff --git a/src/util/statistics_stats.h b/src/util/statistics_stats.h index 0cbe0a99b..e30593041 100644 --- a/src/util/statistics_stats.h +++ b/src/util/statistics_stats.h @@ -73,7 +73,7 @@ class AverageStat * an `std::ostream`. * New values are added by * HistogramStat stat; - * stat << Kind::PLUS << Kind::AND; + * stat << Kind::ADD << Kind::AND; */ template class HistogramStat diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp index fd45b1c22..9af3e9072 100644 --- a/test/unit/api/cpp/op_black.cpp +++ b/test/unit/api/cpp/op_black.cpp @@ -42,13 +42,13 @@ TEST_F(TestApiBlackOp, isNull) TEST_F(TestApiBlackOp, opFromKind) { - ASSERT_NO_THROW(d_solver.mkOp(PLUS)); + ASSERT_NO_THROW(d_solver.mkOp(ADD)); ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC5ApiException); } TEST_F(TestApiBlackOp, getNumIndices) { - Op plus = d_solver.mkOp(PLUS); + Op plus = d_solver.mkOp(ADD); Op divisible = d_solver.mkOp(DIVISIBLE, 4); Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 5); Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); @@ -94,7 +94,7 @@ TEST_F(TestApiBlackOp, getNumIndices) TEST_F(TestApiBlackOp, subscriptOperator) { - Op plus = d_solver.mkOp(PLUS); + Op plus = d_solver.mkOp(ADD); Op divisible = d_solver.mkOp(DIVISIBLE, 4); Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 4); Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 4); diff --git a/test/unit/api/cpp/op_white.cpp b/test/unit/api/cpp/op_white.cpp index 39952739b..3483d409d 100644 --- a/test/unit/api/cpp/op_white.cpp +++ b/test/unit/api/cpp/op_white.cpp @@ -27,10 +27,10 @@ class TestApiWhiteOp : public TestApi TEST_F(TestApiWhiteOp, opFromKind) { - Op plus(&d_solver, PLUS); + Op plus(&d_solver, ADD); ASSERT_FALSE(plus.isIndexed()); ASSERT_THROW(plus.getIndices(), CVC5ApiException); - ASSERT_EQ(plus, d_solver.mkOp(PLUS)); + ASSERT_EQ(plus, d_solver.mkOp(ADD)); } } // namespace test } // namespace cvc5 diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 9f8c6e453..09f0e18ea 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -1417,13 +1417,12 @@ TEST_F(TestApiBlackSolver, getInterpolant) Term z = d_solver.mkConst(intSort, "z"); // Assumptions for interpolation: x + y > 0 /\ x < 0 - d_solver.assertFormula( - d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero)); + d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(ADD, x, y), zero)); d_solver.assertFormula(d_solver.mkTerm(LT, x, zero)); // Conjecture for interpolation: y + z > 0 \/ z < 0 Term conj = d_solver.mkTerm(OR, - d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), + d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero)); Term output; // Call the interpolation api, while the resulting interpolant is the output @@ -1445,13 +1444,12 @@ TEST_F(TestApiBlackSolver, getInterpolantNext) Term y = d_solver.mkConst(intSort, "y"); Term z = d_solver.mkConst(intSort, "z"); // Assumptions for interpolation: x + y > 0 /\ x < 0 - d_solver.assertFormula( - d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero)); + d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(ADD, x, y), zero)); d_solver.assertFormula(d_solver.mkTerm(LT, x, zero)); // Conjecture for interpolation: y + z > 0 \/ z < 0 Term conj = d_solver.mkTerm(OR, - d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), + d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero)); Term output; d_solver.getInterpolant(conj, output); @@ -1647,7 +1645,7 @@ TEST_F(TestApiBlackSolver, getUnsatCoreAndProof) Term one = d_solver.mkInteger(1); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, f_x, f_y); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_x)); @@ -1744,7 +1742,7 @@ TEST_F(TestApiBlackSolver, getValue3) Term one = d_solver.mkInteger(1); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, f_x, f_y); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); @@ -2201,7 +2199,7 @@ TEST_F(TestApiBlackSolver, simplify) ASSERT_NO_THROW(d_solver.simplify(i2)); ASSERT_NE(i1, i2); ASSERT_NE(i1, d_solver.simplify(i2)); - Term i3 = d_solver.mkTerm(PLUS, i1, d_solver.mkInteger(0)); + Term i3 = d_solver.mkTerm(ADD, i1, d_solver.mkInteger(0)); ASSERT_NO_THROW(d_solver.simplify(i3)); ASSERT_NE(i1, i3); ASSERT_EQ(i1, d_solver.simplify(i3)); @@ -2291,7 +2289,7 @@ TEST_F(TestApiBlackSolver, checkEntailed2) // Terms Term f_x = d_solver.mkTerm(APPLY_UF, f, x); Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, f_x, f_y); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); // Assertions @@ -2371,7 +2369,7 @@ TEST_F(TestApiBlackSolver, checkSatAssuming2) // Terms Term f_x = d_solver.mkTerm(APPLY_UF, f, x); Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, f_x, f_y); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); // Assertions diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index c3f418dc4..a4dad3718 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -80,7 +80,7 @@ TEST_F(TestApiBlackTerm, getKind) ASSERT_NO_THROW(f_x.getKind()); Term f_y = d_solver.mkTerm(APPLY_UF, f, y); ASSERT_NO_THROW(f_y.getKind()); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, f_x, f_y); ASSERT_NO_THROW(sum.getKind()); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.getKind()); @@ -129,7 +129,7 @@ TEST_F(TestApiBlackTerm, getSort) Term f_y = d_solver.mkTerm(APPLY_UF, f, y); ASSERT_NO_THROW(f_y.getSort()); ASSERT_EQ(f_y.getSort(), intSort); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, f_x, f_y); ASSERT_NO_THROW(sum.getSort()); ASSERT_EQ(sum.getSort(), intSort); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); @@ -256,7 +256,7 @@ TEST_F(TestApiBlackTerm, notTerm) ASSERT_THROW(zero.notTerm(), CVC5ApiException); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); ASSERT_THROW(f_x.notTerm(), CVC5ApiException); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); ASSERT_THROW(sum.notTerm(), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.notTerm()); @@ -301,7 +301,7 @@ TEST_F(TestApiBlackTerm, andTerm) ASSERT_THROW(f_x.andTerm(p), CVC5ApiException); ASSERT_THROW(f_x.andTerm(zero), CVC5ApiException); ASSERT_THROW(f_x.andTerm(f_x), CVC5ApiException); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); ASSERT_THROW(sum.andTerm(b), CVC5ApiException); ASSERT_THROW(sum.andTerm(x), CVC5ApiException); ASSERT_THROW(sum.andTerm(f), CVC5ApiException); @@ -367,7 +367,7 @@ TEST_F(TestApiBlackTerm, orTerm) ASSERT_THROW(f_x.orTerm(p), CVC5ApiException); ASSERT_THROW(f_x.orTerm(zero), CVC5ApiException); ASSERT_THROW(f_x.orTerm(f_x), CVC5ApiException); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); ASSERT_THROW(sum.orTerm(b), CVC5ApiException); ASSERT_THROW(sum.orTerm(x), CVC5ApiException); ASSERT_THROW(sum.orTerm(f), CVC5ApiException); @@ -433,7 +433,7 @@ TEST_F(TestApiBlackTerm, xorTerm) ASSERT_THROW(f_x.xorTerm(p), CVC5ApiException); ASSERT_THROW(f_x.xorTerm(zero), CVC5ApiException); ASSERT_THROW(f_x.xorTerm(f_x), CVC5ApiException); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); ASSERT_THROW(sum.xorTerm(b), CVC5ApiException); ASSERT_THROW(sum.xorTerm(x), CVC5ApiException); ASSERT_THROW(sum.xorTerm(f), CVC5ApiException); @@ -499,7 +499,7 @@ TEST_F(TestApiBlackTerm, eqTerm) ASSERT_THROW(f_x.eqTerm(p), CVC5ApiException); ASSERT_NO_THROW(f_x.eqTerm(zero)); ASSERT_NO_THROW(f_x.eqTerm(f_x)); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); ASSERT_THROW(sum.eqTerm(b), CVC5ApiException); ASSERT_THROW(sum.eqTerm(x), CVC5ApiException); ASSERT_THROW(sum.eqTerm(f), CVC5ApiException); @@ -565,7 +565,7 @@ TEST_F(TestApiBlackTerm, impTerm) ASSERT_THROW(f_x.impTerm(p), CVC5ApiException); ASSERT_THROW(f_x.impTerm(zero), CVC5ApiException); ASSERT_THROW(f_x.impTerm(f_x), CVC5ApiException); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); ASSERT_THROW(sum.impTerm(b), CVC5ApiException); ASSERT_THROW(sum.impTerm(x), CVC5ApiException); ASSERT_THROW(sum.impTerm(f), CVC5ApiException); @@ -625,7 +625,7 @@ TEST_F(TestApiBlackTerm, iteTerm) Term f_x = d_solver.mkTerm(APPLY_UF, f, x); ASSERT_THROW(f_x.iteTerm(b, b), CVC5ApiException); ASSERT_THROW(f_x.iteTerm(b, x), CVC5ApiException); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); ASSERT_THROW(sum.iteTerm(x, x), CVC5ApiException); ASSERT_THROW(sum.iteTerm(b, x), CVC5ApiException); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); @@ -649,8 +649,8 @@ TEST_F(TestApiBlackTerm, termAssignment) TEST_F(TestApiBlackTerm, termCompare) { Term t1 = d_solver.mkInteger(1); - Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2)); - Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2)); + Term t2 = d_solver.mkTerm(ADD, d_solver.mkInteger(2), d_solver.mkInteger(2)); + Term t3 = d_solver.mkTerm(ADD, d_solver.mkInteger(2), d_solver.mkInteger(2)); ASSERT_TRUE(t2 >= t3); ASSERT_TRUE(t2 <= t3); ASSERT_TRUE((t1 > t2) != (t1 < t2)); @@ -661,7 +661,7 @@ TEST_F(TestApiBlackTerm, termChildren) { // simple term 2+3 Term two = d_solver.mkInteger(2); - Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3)); + Term t1 = d_solver.mkTerm(ADD, two, d_solver.mkInteger(3)); ASSERT_EQ(t1[0], two); ASSERT_EQ(t1.getNumChildren(), 2); Term tnull; @@ -1020,8 +1020,8 @@ TEST_F(TestApiBlackTerm, substitute) Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); Term one = d_solver.mkInteger(1); Term ttrue = d_solver.mkTrue(); - Term xpx = d_solver.mkTerm(PLUS, x, x); - Term onepone = d_solver.mkTerm(PLUS, one, one); + Term xpx = d_solver.mkTerm(ADD, x, x); + Term onepone = d_solver.mkTerm(ADD, one, one); ASSERT_EQ(xpx.substitute(x, one), onepone); ASSERT_EQ(onepone.substitute(one, x), xpx); @@ -1030,8 +1030,8 @@ TEST_F(TestApiBlackTerm, substitute) // simultaneous substitution Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y"); - Term xpy = d_solver.mkTerm(PLUS, x, y); - Term xpone = d_solver.mkTerm(PLUS, y, one); + Term xpy = d_solver.mkTerm(ADD, x, y); + Term xpone = d_solver.mkTerm(ADD, y, one); std::vector es; std::vector rs; es.push_back(x); diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java index 9b4999211..2de478b58 100644 --- a/test/unit/api/java/OpTest.java +++ b/test/unit/api/java/OpTest.java @@ -54,7 +54,7 @@ class OpTest @Test void opFromKind() { - assertDoesNotThrow(() -> d_solver.mkOp(PLUS)); + assertDoesNotThrow(() -> d_solver.mkOp(ADD)); assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT)); } diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 29efbea40..908fed6e5 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1407,11 +1407,11 @@ class SolverTest Term z = d_solver.mkConst(intSort, "z"); // Assumptions for interpolation: x + y > 0 /\ x < 0 - d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero)); + d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(ADD, x, y), zero)); d_solver.assertFormula(d_solver.mkTerm(LT, x, zero)); // Conjecture for interpolation: y + z > 0 \/ z < 0 Term conj = d_solver.mkTerm( - OR, d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), d_solver.mkTerm(LT, z, zero)); + OR, d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero)); Term output = d_solver.getNullTerm(); // Call the interpolation api, while the resulting interpolant is the output d_solver.getInterpolant(conj, output); @@ -1432,10 +1432,10 @@ class SolverTest Term y = d_solver.mkConst(intSort, "y"); Term z = d_solver.mkConst(intSort, "z"); - d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero)); + d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(ADD, x, y), zero)); d_solver.assertFormula(d_solver.mkTerm(LT, x, zero)); Term conj = d_solver.mkTerm( - OR, d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), d_solver.mkTerm(LT, z, zero)); + OR, d_solver.mkTerm(GT, d_solver.mkTerm(ADD, y, z), zero), d_solver.mkTerm(LT, z, zero)); Term output = d_solver.getNullTerm(); d_solver.getInterpolant(conj, output); Term output2 = d_solver.getNullTerm(); @@ -1620,7 +1620,7 @@ class SolverTest Term one = d_solver.mkInteger(1); Term f_x = d_solver.mkTerm(Kind.APPLY_UF, f, x); Term f_y = d_solver.mkTerm(Kind.APPLY_UF, f, y); - Term sum = d_solver.mkTerm(Kind.PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(Kind.ADD, f_x, f_y); Term p_0 = d_solver.mkTerm(Kind.APPLY_UF, p, zero); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); d_solver.assertFormula(d_solver.mkTerm(Kind.GT, zero, f_x)); @@ -1716,7 +1716,7 @@ class SolverTest Term one = d_solver.mkInteger(1); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, f_x, f_y); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); @@ -2176,7 +2176,7 @@ class SolverTest assertDoesNotThrow(() -> d_solver.simplify(i2)); assertNotEquals(i1, i2); assertNotEquals(i1, d_solver.simplify(i2)); - Term i3 = d_solver.mkTerm(PLUS, i1, d_solver.mkInteger(0)); + Term i3 = d_solver.mkTerm(ADD, i1, d_solver.mkInteger(0)); assertDoesNotThrow(() -> d_solver.simplify(i3)); assertNotEquals(i1, i3); assertEquals(i1, d_solver.simplify(i3)); @@ -2269,7 +2269,7 @@ class SolverTest // Terms Term f_x = d_solver.mkTerm(APPLY_UF, f, x); Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, f_x, f_y); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); // Assertions @@ -2353,7 +2353,7 @@ class SolverTest // Terms Term f_x = d_solver.mkTerm(APPLY_UF, f, x); Term f_y = d_solver.mkTerm(APPLY_UF, f, y); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, f_x, f_y); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); // Assertions diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index 6783781de..9baa290af 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -99,7 +99,7 @@ class TermTest assertDoesNotThrow(() -> f_x.getKind()); Term f_y = d_solver.mkTerm(APPLY_UF, f, y); assertDoesNotThrow(() -> f_y.getKind()); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, f_x, f_y); assertDoesNotThrow(() -> sum.getKind()); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); assertDoesNotThrow(() -> p_0.getKind()); @@ -148,7 +148,7 @@ class TermTest Term f_y = d_solver.mkTerm(APPLY_UF, f, y); assertDoesNotThrow(() -> f_y.getSort()); assertEquals(f_y.getSort(), intSort); - Term sum = d_solver.mkTerm(PLUS, f_x, f_y); + Term sum = d_solver.mkTerm(ADD, f_x, f_y); assertDoesNotThrow(() -> sum.getSort()); assertEquals(sum.getSort(), intSort); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); @@ -263,7 +263,7 @@ class TermTest assertThrows(CVC5ApiException.class, () -> zero.notTerm()); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); assertThrows(CVC5ApiException.class, () -> f_x.notTerm()); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); assertThrows(CVC5ApiException.class, () -> sum.notTerm()); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); assertDoesNotThrow(() -> p_0.notTerm()); @@ -308,7 +308,7 @@ class TermTest assertThrows(CVC5ApiException.class, () -> f_x.andTerm(p)); assertThrows(CVC5ApiException.class, () -> f_x.andTerm(zero)); assertThrows(CVC5ApiException.class, () -> f_x.andTerm(f_x)); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); assertThrows(CVC5ApiException.class, () -> sum.andTerm(b)); assertThrows(CVC5ApiException.class, () -> sum.andTerm(x)); assertThrows(CVC5ApiException.class, () -> sum.andTerm(f)); @@ -374,7 +374,7 @@ class TermTest assertThrows(CVC5ApiException.class, () -> f_x.orTerm(p)); assertThrows(CVC5ApiException.class, () -> f_x.orTerm(zero)); assertThrows(CVC5ApiException.class, () -> f_x.orTerm(f_x)); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); assertThrows(CVC5ApiException.class, () -> sum.orTerm(b)); assertThrows(CVC5ApiException.class, () -> sum.orTerm(x)); assertThrows(CVC5ApiException.class, () -> sum.orTerm(f)); @@ -440,7 +440,7 @@ class TermTest assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(p)); assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(zero)); assertThrows(CVC5ApiException.class, () -> f_x.xorTerm(f_x)); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); assertThrows(CVC5ApiException.class, () -> sum.xorTerm(b)); assertThrows(CVC5ApiException.class, () -> sum.xorTerm(x)); assertThrows(CVC5ApiException.class, () -> sum.xorTerm(f)); @@ -506,7 +506,7 @@ class TermTest assertThrows(CVC5ApiException.class, () -> f_x.eqTerm(p)); assertDoesNotThrow(() -> f_x.eqTerm(zero)); assertDoesNotThrow(() -> f_x.eqTerm(f_x)); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); assertThrows(CVC5ApiException.class, () -> sum.eqTerm(b)); assertThrows(CVC5ApiException.class, () -> sum.eqTerm(x)); assertThrows(CVC5ApiException.class, () -> sum.eqTerm(f)); @@ -572,7 +572,7 @@ class TermTest assertThrows(CVC5ApiException.class, () -> f_x.impTerm(p)); assertThrows(CVC5ApiException.class, () -> f_x.impTerm(zero)); assertThrows(CVC5ApiException.class, () -> f_x.impTerm(f_x)); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); assertThrows(CVC5ApiException.class, () -> sum.impTerm(b)); assertThrows(CVC5ApiException.class, () -> sum.impTerm(x)); assertThrows(CVC5ApiException.class, () -> sum.impTerm(f)); @@ -632,7 +632,7 @@ class TermTest Term f_x = d_solver.mkTerm(APPLY_UF, f, x); assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, b)); assertThrows(CVC5ApiException.class, () -> f_x.iteTerm(b, x)); - Term sum = d_solver.mkTerm(PLUS, f_x, f_x); + Term sum = d_solver.mkTerm(ADD, f_x, f_x); assertThrows(CVC5ApiException.class, () -> sum.iteTerm(x, x)); assertThrows(CVC5ApiException.class, () -> sum.iteTerm(b, x)); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); @@ -656,8 +656,8 @@ class TermTest @Test void termCompare() { Term t1 = d_solver.mkInteger(1); - Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2)); - Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2)); + Term t2 = d_solver.mkTerm(ADD, d_solver.mkInteger(2), d_solver.mkInteger(2)); + Term t3 = d_solver.mkTerm(ADD, d_solver.mkInteger(2), d_solver.mkInteger(2)); assertTrue(t2.compareTo(t3) >= 0); assertTrue(t2.compareTo(t3) <= 0); assertTrue((t1.compareTo(t2) > 0) != (t1.compareTo(t2) < 0)); @@ -668,7 +668,7 @@ class TermTest { // simple term 2+3 Term two = d_solver.mkInteger(2); - Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3)); + Term t1 = d_solver.mkTerm(ADD, two, d_solver.mkInteger(3)); assertEquals(t1.getChild(0), two); assertEquals(t1.getNumChildren(), 2); Term tnull = d_solver.getNullTerm(); @@ -977,8 +977,8 @@ class TermTest Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); Term one = d_solver.mkInteger(1); Term ttrue = d_solver.mkTrue(); - Term xpx = d_solver.mkTerm(PLUS, x, x); - Term onepone = d_solver.mkTerm(PLUS, one, one); + Term xpx = d_solver.mkTerm(ADD, x, x); + Term onepone = d_solver.mkTerm(ADD, one, one); assertEquals(xpx.substitute(x, one), onepone); assertEquals(onepone.substitute(one, x), xpx); @@ -987,8 +987,8 @@ class TermTest // simultaneous substitution Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y"); - Term xpy = d_solver.mkTerm(PLUS, x, y); - Term xpone = d_solver.mkTerm(PLUS, y, one); + Term xpy = d_solver.mkTerm(ADD, x, y); + Term xpone = d_solver.mkTerm(ADD, y, one); List es = new ArrayList<>(); List rs = new ArrayList<>(); es.add(x); diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py index 34ce89b3b..4059a4fb0 100644 --- a/test/unit/api/python/test_op.py +++ b/test/unit/api/python/test_op.py @@ -40,13 +40,13 @@ def test_is_null(solver): def test_op_from_kind(solver): - solver.mkOp(Kind.Plus) + solver.mkOp(Kind.Add) with pytest.raises(RuntimeError): solver.mkOp(Kind.BVExtract) def test_get_num_indices(solver): - plus = solver.mkOp(Kind.Plus) + plus = solver.mkOp(Kind.Add) divisible = solver.mkOp(Kind.Divisible, 4) bitvector_repeat = solver.mkOp(Kind.BVRepeat, 5) bitvector_zero_extend = solver.mkOp(Kind.BVZeroExtend, 6) diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index a2abcf847..d0e2094f9 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -1241,7 +1241,7 @@ def test_get_unsat_core3(solver): one = solver.mkInteger(1) f_x = solver.mkTerm(Kind.ApplyUf, f, x) f_y = solver.mkTerm(Kind.ApplyUf, f, y) - summ = solver.mkTerm(Kind.Plus, f_x, f_y) + summ = solver.mkTerm(Kind.Add, f_x, f_y) p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_x)) @@ -1295,7 +1295,7 @@ def test_get_value3(solver): one = solver.mkInteger(1) f_x = solver.mkTerm(Kind.ApplyUf, f, x) f_y = solver.mkTerm(Kind.ApplyUf, f, y) - summ = solver.mkTerm(Kind.Plus, f_x, f_y) + summ = solver.mkTerm(Kind.Add, f_x, f_y) p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) @@ -1545,7 +1545,7 @@ def test_simplify(solver): solver.simplify(i2) assert i1 != i2 assert i1 != solver.simplify(i2) - i3 = solver.mkTerm(Kind.Plus, i1, solver.mkInteger(0)) + i3 = solver.mkTerm(Kind.Add, i1, solver.mkInteger(0)) solver.simplify(i3) assert i1 != i3 assert i1 == solver.simplify(i3) @@ -1637,7 +1637,7 @@ def test_check_entailed2(solver): # Terms f_x = solver.mkTerm(Kind.ApplyUf, f, x) f_y = solver.mkTerm(Kind.ApplyUf, f, y) - summ = solver.mkTerm(Kind.Plus, f_x, f_y) + summ = solver.mkTerm(Kind.Add, f_x, f_y) p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) # Assertions @@ -1719,7 +1719,7 @@ def test_check_sat_assuming2(solver): # Terms f_x = solver.mkTerm(Kind.ApplyUf, f, x) f_y = solver.mkTerm(Kind.ApplyUf, f, y) - summ = solver.mkTerm(Kind.Plus, f_x, f_y) + summ = solver.mkTerm(Kind.Add, f_x, f_y) p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) # Assertions @@ -2037,9 +2037,13 @@ def test_get_interpolant(solver): y = solver.mkConst(intSort, "y") z = solver.mkConst(intSort, "z") - solver.assertFormula(solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, x, y), zero)) + solver.assertFormula(solver.mkTerm( + Kind.Gt, solver.mkTerm(Kind.Add, x, y), zero)) solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero)) - conj = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, y, z), zero), solver.mkTerm(Kind.Lt, z, zero)) + conj = solver.mkTerm( + Kind.Or, + solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero), + solver.mkTerm(Kind.Lt, z, zero)) output = cvc5.Term(solver) solver.getInterpolant(conj, output) assert output.getSort().isBoolean() @@ -2055,9 +2059,13 @@ def test_get_interpolant_next(solver): y = solver.mkConst(intSort, "y") z = solver.mkConst(intSort, "z") - solver.assertFormula(solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, x, y), zero)) + solver.assertFormula(solver.mkTerm( + Kind.Gt, solver.mkTerm(Kind.Add, x, y), zero)) solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero)) - conj = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, y, z), zero), solver.mkTerm(Kind.Lt, z, zero)) + conj = solver.mkTerm( + Kind.Or, + solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Add, y, z), zero), + solver.mkTerm(Kind.Lt, z, zero)) output = cvc5.Term(solver) solver.getInterpolant(conj, output) output2 = cvc5.Term(solver) diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index f1f075785..27d1d913e 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -77,7 +77,7 @@ def test_get_kind(solver): f_x.getKind() f_y = solver.mkTerm(Kind.ApplyUf, f, y) f_y.getKind() - sum = solver.mkTerm(Kind.Plus, f_x, f_y) + sum = solver.mkTerm(Kind.Add, f_x, f_y) sum.getKind() p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.getKind() @@ -126,7 +126,7 @@ def test_get_sort(solver): f_y = solver.mkTerm(Kind.ApplyUf, f, y) f_y.getSort() assert f_y.getSort() == intSort - sum = solver.mkTerm(Kind.Plus, f_x, f_y) + sum = solver.mkTerm(Kind.Add, f_x, f_y) sum.getSort() assert sum.getSort() == intSort p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) @@ -258,7 +258,7 @@ def test_not_term(solver): f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.notTerm() - sum = solver.mkTerm(Kind.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Add, f_x, f_x) with pytest.raises(RuntimeError): sum.notTerm() p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) @@ -325,7 +325,7 @@ def test_and_term(solver): f_x.andTerm(zero) with pytest.raises(RuntimeError): f_x.andTerm(f_x) - sum = solver.mkTerm(Kind.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Add, f_x, f_x) with pytest.raises(RuntimeError): sum.andTerm(b) with pytest.raises(RuntimeError): @@ -431,7 +431,7 @@ def test_or_term(solver): f_x.orTerm(zero) with pytest.raises(RuntimeError): f_x.orTerm(f_x) - sum = solver.mkTerm(Kind.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Add, f_x, f_x) with pytest.raises(RuntimeError): sum.orTerm(b) with pytest.raises(RuntimeError): @@ -537,7 +537,7 @@ def test_xor_term(solver): f_x.xorTerm(zero) with pytest.raises(RuntimeError): f_x.xorTerm(f_x) - sum = solver.mkTerm(Kind.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Add, f_x, f_x) with pytest.raises(RuntimeError): sum.xorTerm(b) with pytest.raises(RuntimeError): @@ -637,7 +637,7 @@ def test_eq_term(solver): f_x.eqTerm(p) f_x.eqTerm(zero) f_x.eqTerm(f_x) - sum = solver.mkTerm(Kind.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Add, f_x, f_x) with pytest.raises(RuntimeError): sum.eqTerm(b) with pytest.raises(RuntimeError): @@ -740,7 +740,7 @@ def test_imp_term(solver): f_x.impTerm(zero) with pytest.raises(RuntimeError): f_x.impTerm(f_x) - sum = solver.mkTerm(Kind.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Add, f_x, f_x) with pytest.raises(RuntimeError): sum.impTerm(b) with pytest.raises(RuntimeError): @@ -832,7 +832,7 @@ def test_ite_term(solver): f_x.iteTerm(b, b) with pytest.raises(RuntimeError): f_x.iteTerm(b, x) - sum = solver.mkTerm(Kind.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Add, f_x, f_x) with pytest.raises(RuntimeError): sum.iteTerm(x, x) with pytest.raises(RuntimeError): @@ -860,8 +860,8 @@ def test_substitute(solver): x = solver.mkConst(solver.getIntegerSort(), "x") one = solver.mkInteger(1) ttrue = solver.mkTrue() - xpx = solver.mkTerm(Kind.Plus, x, x) - onepone = solver.mkTerm(Kind.Plus, one, one) + xpx = solver.mkTerm(Kind.Add, x, x) + onepone = solver.mkTerm(Kind.Add, one, one) assert xpx.substitute(x, one) == onepone assert onepone.substitute(one, x) == xpx @@ -871,8 +871,8 @@ def test_substitute(solver): # simultaneous substitution y = solver.mkConst(solver.getIntegerSort(), "y") - xpy = solver.mkTerm(Kind.Plus, x, y) - xpone = solver.mkTerm(Kind.Plus, y, one) + xpy = solver.mkTerm(Kind.Add, x, y) + xpone = solver.mkTerm(Kind.Add, y, one) es = [] rs = [] es.append(x) @@ -917,8 +917,8 @@ def test_substitute(solver): def test_term_compare(solver): t1 = solver.mkInteger(1) - t2 = solver.mkTerm(Kind.Plus, solver.mkInteger(2), solver.mkInteger(2)) - t3 = solver.mkTerm(Kind.Plus, solver.mkInteger(2), solver.mkInteger(2)) + t2 = solver.mkTerm(Kind.Add, solver.mkInteger(2), solver.mkInteger(2)) + t3 = solver.mkTerm(Kind.Add, solver.mkInteger(2), solver.mkInteger(2)) assert t2 >= t3 assert t2 <= t3 assert (t1 > t2) != (t1 < t2) @@ -928,7 +928,7 @@ def test_term_compare(solver): def test_term_children(solver): # simple term 2+3 two = solver.mkInteger(2) - t1 = solver.mkTerm(Kind.Plus, two, solver.mkInteger(3)) + t1 = solver.mkTerm(Kind.Add, two, solver.mkInteger(3)) assert t1[0] == two assert t1.getNumChildren() == 2 tnull = Term(solver) diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index 8dac2cfda..7fa2b6bfe 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -61,7 +61,7 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2) Node var = d_nodeManager->mkBoundVar(*d_intTypeNode); std::vector vars; vars.push_back(var); - Node sum = d_nodeManager->mkNode(PLUS, var, var); + Node sum = d_nodeManager->mkNode(ADD, var, var); Node qeq = d_nodeManager->mkNode(EQUAL, x, sum); Node bvl = d_nodeManager->mkNode(BOUND_VAR_LIST, vars); Node right = d_nodeManager->mkNode(EXISTS, bvl, qeq); @@ -88,7 +88,7 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map) // create test formula Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType()); - Node plus = d_nodeManager->mkNode(PLUS, x, x); + Node plus = d_nodeManager->mkNode(ADD, x, x); Node mul = d_nodeManager->mkNode(MULT, x, x); Node eq1 = d_nodeManager->mkNode(EQUAL, plus, mul); @@ -112,7 +112,7 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map) // in integers, we should only have plus and mult as operators ASSERT_EQ(result[*d_intTypeNode].size(), 2); - ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)), + ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(ADD)), result[*d_intTypeNode].end()); ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)), result[*d_intTypeNode].end()); diff --git a/test/unit/node/node_algorithms_black.cpp b/test/unit/node/node_algorithms_black.cpp index ebcb9b6c1..eb54a6b7f 100644 --- a/test/unit/node/node_algorithms_black.cpp +++ b/test/unit/node/node_algorithms_black.cpp @@ -33,15 +33,15 @@ TEST_F(TestNodeBlackNodeAlgorithms, flatten) { { Node x = d_nodeManager->mkBoundVar(*d_realTypeNode); - Node n = d_nodeManager->mkNode(Kind::PLUS, x, x); + Node n = d_nodeManager->mkNode(Kind::ADD, x, x); EXPECT_FALSE(expr::algorithm::canFlatten(n)); - EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::PLUS)); + EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::ADD)); EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::MULT)); - EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::PLUS, Kind::MULT)); + EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::ADD, Kind::MULT)); EXPECT_EQ(expr::algorithm::flatten(n), n); - EXPECT_EQ(expr::algorithm::flatten(n, Kind::PLUS), n); + EXPECT_EQ(expr::algorithm::flatten(n, Kind::ADD), n); EXPECT_EQ(expr::algorithm::flatten(n, Kind::MULT), n); - EXPECT_EQ(expr::algorithm::flatten(n, Kind::PLUS, Kind::MULT), n); + EXPECT_EQ(expr::algorithm::flatten(n, Kind::ADD, Kind::MULT), n); { std::vector children; @@ -52,7 +52,7 @@ TEST_F(TestNodeBlackNodeAlgorithms, flatten) } { std::vector children; - expr::algorithm::flatten(n, children, Kind::PLUS); + expr::algorithm::flatten(n, children, Kind::ADD); EXPECT_EQ(children.size(), 2); EXPECT_EQ(children[0], x); EXPECT_EQ(children[1], x); @@ -65,7 +65,7 @@ TEST_F(TestNodeBlackNodeAlgorithms, flatten) } { std::vector children; - expr::algorithm::flatten(n, children, Kind::PLUS, Kind::MULT); + expr::algorithm::flatten(n, children, Kind::ADD, Kind::MULT); EXPECT_EQ(children.size(), 2); EXPECT_EQ(children[0], x); EXPECT_EQ(children[1], x); @@ -74,15 +74,15 @@ TEST_F(TestNodeBlackNodeAlgorithms, flatten) { Node x = d_nodeManager->mkBoundVar(*d_realTypeNode); Node n = d_nodeManager->mkNode( - Kind::PLUS, x, d_nodeManager->mkNode(Kind::PLUS, x, x)); + Kind::ADD, x, d_nodeManager->mkNode(Kind::ADD, x, x)); EXPECT_TRUE(expr::algorithm::canFlatten(n)); - EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::PLUS)); + EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::ADD)); EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::MULT)); - EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::PLUS, Kind::MULT)); + EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::ADD, Kind::MULT)); EXPECT_NE(expr::algorithm::flatten(n), n); - EXPECT_NE(expr::algorithm::flatten(n, Kind::PLUS), n); + EXPECT_NE(expr::algorithm::flatten(n, Kind::ADD), n); EXPECT_EQ(expr::algorithm::flatten(n, Kind::MULT), n); - EXPECT_NE(expr::algorithm::flatten(n, Kind::PLUS, Kind::MULT), n); + EXPECT_NE(expr::algorithm::flatten(n, Kind::ADD, Kind::MULT), n); { std::vector children; @@ -94,7 +94,7 @@ TEST_F(TestNodeBlackNodeAlgorithms, flatten) } { std::vector children; - expr::algorithm::flatten(n, children, Kind::PLUS); + expr::algorithm::flatten(n, children, Kind::ADD); EXPECT_EQ(children.size(), 3); EXPECT_EQ(children[0], x); EXPECT_EQ(children[1], x); @@ -108,7 +108,7 @@ TEST_F(TestNodeBlackNodeAlgorithms, flatten) } { std::vector children; - expr::algorithm::flatten(n, children, Kind::PLUS, Kind::MULT); + expr::algorithm::flatten(n, children, Kind::ADD, Kind::MULT); EXPECT_EQ(children.size(), 3); EXPECT_EQ(children[0], x); EXPECT_EQ(children[1], x); @@ -118,15 +118,15 @@ TEST_F(TestNodeBlackNodeAlgorithms, flatten) { Node x = d_nodeManager->mkBoundVar(*d_realTypeNode); Node n = d_nodeManager->mkNode( - Kind::PLUS, x, d_nodeManager->mkNode(Kind::MULT, x, x)); + Kind::ADD, x, d_nodeManager->mkNode(Kind::MULT, x, x)); EXPECT_FALSE(expr::algorithm::canFlatten(n)); - EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::PLUS)); + EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::ADD)); EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::MULT)); - EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::PLUS, Kind::MULT)); + EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::ADD, Kind::MULT)); EXPECT_EQ(expr::algorithm::flatten(n), n); - EXPECT_EQ(expr::algorithm::flatten(n, Kind::PLUS), n); + EXPECT_EQ(expr::algorithm::flatten(n, Kind::ADD), n); EXPECT_EQ(expr::algorithm::flatten(n, Kind::MULT), n); - EXPECT_NE(expr::algorithm::flatten(n, Kind::PLUS, Kind::MULT), n); + EXPECT_NE(expr::algorithm::flatten(n, Kind::ADD, Kind::MULT), n); { std::vector children; @@ -137,7 +137,7 @@ TEST_F(TestNodeBlackNodeAlgorithms, flatten) } { std::vector children; - expr::algorithm::flatten(n, children, Kind::PLUS); + expr::algorithm::flatten(n, children, Kind::ADD); EXPECT_EQ(children.size(), 2); EXPECT_EQ(children[0], x); EXPECT_EQ(children[1], n[1]); @@ -150,7 +150,7 @@ TEST_F(TestNodeBlackNodeAlgorithms, flatten) } { std::vector children; - expr::algorithm::flatten(n, children, Kind::PLUS, Kind::MULT); + expr::algorithm::flatten(n, children, Kind::ADD, Kind::MULT); EXPECT_EQ(children.size(), 3); EXPECT_EQ(children[0], x); EXPECT_EQ(children[1], x); diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 623a38c81..a1486df94 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -398,8 +398,8 @@ TEST_F(TestNodeBlackNode, getKind) Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->realType()); Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->realType()); - n = d_nodeManager->mkNode(PLUS, x, y); - ASSERT_EQ(PLUS, n.getKind()); + n = d_nodeManager->mkNode(ADD, x, y); + ASSERT_EQ(ADD, n.getKind()); n = d_nodeManager->mkNode(NEG, x); ASSERT_EQ(NEG, n.getKind()); @@ -512,19 +512,19 @@ TEST_F(TestNodeBlackNode, kinded_iterator) Node x = d_skolemManager->mkDummySkolem("x", integerType); Node y = d_skolemManager->mkDummySkolem("y", integerType); Node z = d_skolemManager->mkDummySkolem("z", integerType); - Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z); + Node plus_x_y_z = d_nodeManager->mkNode(kind::ADD, x, y, z); Node x_minus_y = d_nodeManager->mkNode(kind::SUB, x, y); { // iterator - Node::kinded_iterator i = plus_x_y_z.begin(PLUS); + Node::kinded_iterator i = plus_x_y_z.begin(ADD); ASSERT_EQ(*i++, x); ASSERT_EQ(*i++, y); ASSERT_EQ(*i++, z); - ASSERT_TRUE(i == plus_x_y_z.end(PLUS)); + ASSERT_TRUE(i == plus_x_y_z.end(ADD)); - i = x.begin(PLUS); + i = x.begin(ADD); ASSERT_EQ(*i++, x); - ASSERT_TRUE(i == x.end(PLUS)); + ASSERT_TRUE(i == x.end(ADD)); } } @@ -659,7 +659,7 @@ TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node) { const std::vector skolems = makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); - Node add = d_nodeManager->mkNode(kind::PLUS, skolems); + Node add = d_nodeManager->mkNode(kind::ADD, skolems); std::vector children; for (Node child : add) { @@ -673,7 +673,7 @@ TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode) { const std::vector skolems = makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); - Node add = d_nodeManager->mkNode(kind::PLUS, skolems); + Node add = d_nodeManager->mkNode(kind::ADD, skolems); std::vector children; for (TNode child : add) { @@ -687,7 +687,7 @@ TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node) { const std::vector skolems = makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); - Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems); + Node add_node = d_nodeManager->mkNode(kind::ADD, skolems); TNode add_tnode = add_node; std::vector children; for (Node child : add_tnode) @@ -702,7 +702,7 @@ TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode) { const std::vector skolems = makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); - Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems); + Node add_node = d_nodeManager->mkNode(kind::ADD, skolems); TNode add_tnode = add_node; std::vector children; for (TNode child : add_tnode) diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index d9be92249..8e5a870bf 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -95,18 +95,18 @@ TEST_F(TestNodeBlackNodeBuilder, getKind) noKind << x << x; ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND); - noKind << PLUS; - ASSERT_EQ(noKind.getKind(), PLUS); + noKind << ADD; + ASSERT_EQ(noKind.getKind(), ADD); Node n = noKind; #ifdef CVC5_ASSERTIONS ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)"); #endif - NodeBuilder spec(PLUS); - ASSERT_EQ(spec.getKind(), PLUS); + NodeBuilder spec(ADD); + ASSERT_EQ(spec.getKind(), ADD); spec << x << x; - ASSERT_EQ(spec.getKind(), PLUS); + ASSERT_EQ(spec.getKind(), ADD); } TEST_F(TestNodeBlackNodeBuilder, getNumChildren) @@ -118,7 +118,7 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren) ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif - nb << PLUS << x << x; + nb << ADD << x << x; ASSERT_EQ(nb.getNumChildren(), 2u); nb << x << x; @@ -129,7 +129,7 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren) ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif - nb.clear(PLUS); + nb.clear(ADD); ASSERT_EQ(nb.getNumChildren(), 0u); nb << x << x << x; @@ -139,7 +139,7 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren) ASSERT_EQ(nb.getNumChildren(), 6u); #ifdef CVC5_ASSERTIONS - ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb << ADD, "getKind\\(\\) == kind::UNDEFINED_KIND"); Node n = nb; ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)"); #endif @@ -229,7 +229,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind) { #ifdef CVC5_ASSERTIONS NodeBuilder spec(d_specKind); - ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder"); + ASSERT_DEATH(spec << ADD, "can't redefine the Kind of a NodeBuilder"); #endif NodeBuilder noSpec; @@ -243,16 +243,16 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind) NodeBuilder nb(d_specKind); nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false); - nb.clear(PLUS); + nb.clear(ADD); #ifdef CVC5_ASSERTIONS Node n; - ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children"); - nb.clear(PLUS); + ASSERT_DEATH(n = nb, "Nodes with kind ADD must have at least 2 children"); + nb.clear(ADD); #endif #ifdef CVC5_ASSERTIONS - ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder"); + ASSERT_DEATH(nb << ADD, "can't redefine the Kind of a NodeBuilder"); #endif NodeBuilder testRef; @@ -260,7 +260,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind) #ifdef CVC5_ASSERTIONS NodeBuilder testTwo; - ASSERT_DEATH(testTwo << d_specKind << PLUS, + ASSERT_DEATH(testTwo << d_specKind << ADD, "can't redefine the Kind of a NodeBuilder"); #endif @@ -313,7 +313,7 @@ TEST_F(TestNodeBlackNodeBuilder, append) Node p = d_nodeManager->mkNode( EQUAL, d_nodeManager->mkConst(CONST_RATIONAL, 0), - d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(NEG, s), t)); + d_nodeManager->mkNode(ADD, r, d_nodeManager->mkNode(NEG, s), t)); Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y)); #ifdef CVC5_ASSERTIONS diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp index 8061526d5..f1d46c3ec 100644 --- a/test/unit/node/node_white.cpp +++ b/test/unit/node/node_white.cpp @@ -48,11 +48,11 @@ TEST_F(TestNodeWhiteNode, iterators) { Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType()); Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType()); - Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y); + Node x_plus_y = d_nodeManager->mkNode(ADD, x, y); Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); Node x_times_2 = d_nodeManager->mkNode(MULT, x, two); - Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y); + Node n = d_nodeManager->mkNode(ADD, x_times_2, x_plus_y, y); Node::iterator i; diff --git a/test/unit/theory/arith_poly_white.cpp b/test/unit/theory/arith_poly_white.cpp index 989651aee..adfa59f0e 100644 --- a/test/unit/theory/arith_poly_white.cpp +++ b/test/unit/theory/arith_poly_white.cpp @@ -54,45 +54,45 @@ TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int) t2 = one; ASSERT_FALSE(PolyNorm::isArithPolyNorm(t1, t2)); - t1 = d_nodeManager->mkNode(PLUS, x, y); - t2 = d_nodeManager->mkNode(PLUS, y, d_nodeManager->mkNode(MULT, one, x)); + t1 = d_nodeManager->mkNode(ADD, x, y); + t2 = d_nodeManager->mkNode(ADD, y, d_nodeManager->mkNode(MULT, one, x)); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); - t2 = d_nodeManager->mkNode(PLUS, x, x, y); + t2 = d_nodeManager->mkNode(ADD, x, x, y); ASSERT_FALSE(PolyNorm::isArithPolyNorm(t1, t2)); - t1 = d_nodeManager->mkNode(PLUS, x, d_nodeManager->mkNode(MULT, y, zero)); + t1 = d_nodeManager->mkNode(ADD, x, d_nodeManager->mkNode(MULT, y, zero)); t2 = x; ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); - t1 = d_nodeManager->mkNode(MULT, y, d_nodeManager->mkNode(PLUS, one, one)); - t2 = d_nodeManager->mkNode(PLUS, y, y); + t1 = d_nodeManager->mkNode(MULT, y, d_nodeManager->mkNode(ADD, one, one)); + t2 = d_nodeManager->mkNode(ADD, y, y); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); t1 = d_nodeManager->mkNode(MULT, - d_nodeManager->mkNode(PLUS, one, zero), - d_nodeManager->mkNode(PLUS, x, y)); - t2 = d_nodeManager->mkNode(PLUS, x, y); + d_nodeManager->mkNode(ADD, one, zero), + d_nodeManager->mkNode(ADD, x, y)); + t2 = d_nodeManager->mkNode(ADD, x, y); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); - t1 = d_nodeManager->mkNode(PLUS, {x, y, z, w, y}); - t2 = d_nodeManager->mkNode(PLUS, {w, y, y, z, x}); + t1 = d_nodeManager->mkNode(ADD, {x, y, z, w, y}); + t2 = d_nodeManager->mkNode(ADD, {w, y, y, z, x}); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); t1 = d_nodeManager->mkNode(SUB, t1, t2); t2 = zero; ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); - t1 = d_nodeManager->mkNode(NEG, d_nodeManager->mkNode(PLUS, x, y)); - t2 = d_nodeManager->mkNode(SUB, zero, d_nodeManager->mkNode(PLUS, y, x)); + t1 = d_nodeManager->mkNode(NEG, d_nodeManager->mkNode(ADD, x, y)); + t2 = d_nodeManager->mkNode(SUB, zero, d_nodeManager->mkNode(ADD, y, x)); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); t1 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(NEG, x), y); t2 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(NEG, y), x); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); - t1 = d_nodeManager->mkNode(MULT, x, d_nodeManager->mkNode(PLUS, y, z)); - t2 = d_nodeManager->mkNode(PLUS, + t1 = d_nodeManager->mkNode(MULT, x, d_nodeManager->mkNode(ADD, y, z)); + t2 = d_nodeManager->mkNode(ADD, d_nodeManager->mkNode(MULT, x, y), d_nodeManager->mkNode(MULT, z, x)); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); @@ -110,18 +110,18 @@ TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_real) Node t1, t2; - t1 = d_nodeManager->mkNode(PLUS, x, y, y); - t2 = d_nodeManager->mkNode(PLUS, y, x, y); + t1 = d_nodeManager->mkNode(ADD, x, y, y); + t2 = d_nodeManager->mkNode(ADD, y, x, y); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); t1 = one; t2 = d_nodeManager->mkNode(MULT, two, half); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); - t1 = d_nodeManager->mkNode(PLUS, y, x); + t1 = d_nodeManager->mkNode(ADD, y, x); t2 = d_nodeManager->mkNode( MULT, - d_nodeManager->mkNode(PLUS, + d_nodeManager->mkNode(ADD, d_nodeManager->mkNode(MULT, half, x), d_nodeManager->mkNode(MULT, half, y)), two); diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index 71f6c240c..5ba583455 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -157,7 +157,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) Node a = d_nodeManager->mkConst(::cvc5::String("A")); Node slen_y = d_nodeManager->mkNode(kind::STRING_LENGTH, y); - Node x_plus_slen_y = d_nodeManager->mkNode(kind::PLUS, x, slen_y); + Node x_plus_slen_y = d_nodeManager->mkNode(kind::ADD, x, slen_y); Node x_plus_slen_y_eq_zero = d_rewriter->rewrite( d_nodeManager->mkNode(kind::EQUAL, x_plus_slen_y, zero)); @@ -168,7 +168,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) ASSERT_FALSE(ae.checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, true)); Node x_plus_slen_y_plus_z_eq_zero = d_rewriter->rewrite(d_nodeManager->mkNode( - kind::EQUAL, d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, z), zero)); + kind::EQUAL, d_nodeManager->mkNode(kind::ADD, x_plus_slen_y, z), zero)); // x + (str.len y) + z = 0 |= 0 > x --> false ASSERT_FALSE( @@ -177,7 +177,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) Node x_plus_slen_y_plus_slen_y_eq_zero = d_rewriter->rewrite(d_nodeManager->mkNode( kind::EQUAL, - d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, slen_y), + d_nodeManager->mkNode(kind::ADD, x_plus_slen_y, slen_y), zero)); // x + (str.len y) + (str.len y) = 0 |= 0 >= x --> true @@ -186,7 +186,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) Node five = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)); Node six = d_nodeManager->mkConst(CONST_RATIONAL, Rational(6)); - Node x_plus_five = d_nodeManager->mkNode(kind::PLUS, x, five); + Node x_plus_five = d_nodeManager->mkNode(kind::ADD, x, five); Node x_plus_five_lt_six = d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six)); @@ -299,7 +299,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) kind::STRING_SUBSTR, a, d_nodeManager->mkNode( - kind::PLUS, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))), + kind::ADD, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))), x); sameNormalForm(n, empty); @@ -308,7 +308,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) kind::STRING_SUBSTR, a, d_nodeManager->mkNode( - kind::PLUS, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)), + kind::ADD, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)), x); sameNormalForm(n, empty); @@ -318,15 +318,13 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) ASSERT_EQ(res, n); // (str.substr "ABCD" (+ x 3) x) -> "" - n = d_nodeManager->mkNode(kind::STRING_SUBSTR, - abcd, - d_nodeManager->mkNode(kind::PLUS, x, three), - x); + n = d_nodeManager->mkNode( + kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::ADD, x, three), x); sameNormalForm(n, empty); // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x) n = d_nodeManager->mkNode( - kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::PLUS, x, two), x); + kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::ADD, x, two), x); res = sr.rewriteSubstr(n); sameNormalForm(res, n); @@ -683,7 +681,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf) a, zero); Node rhs = d_nodeManager->mkNode( - kind::PLUS, + kind::ADD, two, d_nodeManager->mkNode( kind::STRING_INDEXOF, diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp index 1f85e88d0..75425eba4 100644 --- a/test/unit/theory/theory_arith_cad_white.cpp +++ b/test/unit/theory/theory_arith_cad_white.cpp @@ -85,7 +85,7 @@ Node operator>=(const Node& a, const Node& b) } Node operator+(const Node& a, const Node& b) { - return nodeManager->mkNode(Kind::PLUS, a, b); + return nodeManager->mkNode(Kind::ADD, a, b); } Node operator*(const Node& a, const Node& b) { @@ -191,7 +191,7 @@ TEST_F(TestTheoryWhiteArithCAD, lazard_simp) d_nodeManager->mkNode( Kind::EQUAL, d_nodeManager->mkNode( - Kind::PLUS, + Kind::ADD, d_nodeManager->mkNode(Kind::NONLINEAR_MULT, a, c), d_nodeManager->mkConst(CONST_RATIONAL, d_one)), d_nodeManager->mkConst(CONST_RATIONAL, d_zero))}); diff --git a/test/unit/theory/theory_arith_rewriter_black.cpp b/test/unit/theory/theory_arith_rewriter_black.cpp index b3746db15..059923769 100644 --- a/test/unit/theory/theory_arith_rewriter_black.cpp +++ b/test/unit/theory/theory_arith_rewriter_black.cpp @@ -42,7 +42,7 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber) RealAlgebraicNumber twosqrt2({-8, 0, 1}, 2, 3); RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 3); Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2); - n = d_nodeManager->mkNode(Kind::PLUS, n, n); + n = d_nodeManager->mkNode(Kind::ADD, n, n); n = d_slvEngine->getRewriter()->rewrite(n); EXPECT_EQ(n.getKind(), Kind::REAL_ALGEBRAIC_NUMBER); EXPECT_EQ(n.getOperator().getConst(), twosqrt2); diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 8805c7119..d22dd4e04 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -118,7 +118,7 @@ TEST_F(TestTheoryWhiteArith, int_normal_form) // (exp (+ 2 + x)) --> (* (exp x) (exp 1) (exp 1)) Node t = - d_nodeManager->mkNode(EXPONENTIAL, d_nodeManager->mkNode(PLUS, c2, xr)) + d_nodeManager->mkNode(EXPONENTIAL, d_nodeManager->mkNode(ADD, c2, xr)) .eqNode(c0); ASSERT_EQ(Rewriter::rewrite(Rewriter::rewrite(t)), Rewriter::rewrite(t)); } diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index af24abc39..6f57cab99 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -683,7 +683,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_card) Node n3 = d_nodeManager->mkNode(BAG_CARD, unionDisjointAB); Node cardA = d_nodeManager->mkNode(BAG_CARD, A); Node cardB = d_nodeManager->mkNode(BAG_CARD, B); - Node plus = d_nodeManager->mkNode(PLUS, cardA, cardB); + Node plus = d_nodeManager->mkNode(ADD, cardA, cardB); RewriteResponse response3 = d_rewriter->postRewrite(n3); ASSERT_TRUE(response3.d_node == plus && response3.d_status == REWRITE_AGAIN_FULL); @@ -812,7 +812,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, fold) Node x = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType()); Node y = d_nodeManager->mkBoundVar("y", d_nodeManager->integerType()); Node xy = d_nodeManager->mkNode(BOUND_VAR_LIST, x, y); - Node sum = d_nodeManager->mkNode(PLUS, x, y); + Node sum = d_nodeManager->mkNode(ADD, x, y); // f(x,y) = 0 for all x, y Node f = d_nodeManager->mkNode(LAMBDA, xy, zero); diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp index 9aeedbfe6..24bac4c20 100644 --- a/test/unit/theory/theory_engine_white.cpp +++ b/test/unit/theory/theory_engine_white.cpp @@ -79,10 +79,10 @@ TEST_F(TestTheoryWhiteEngine, rewriter_simple) Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType()); Node z = d_nodeManager->mkVar("z", d_nodeManager->integerType()); - // make the expression (PLUS x y (MULT z 0)) + // make the expression (ADD x y (MULT z 0)) Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0")); Node zTimesZero = d_nodeManager->mkNode(MULT, z, zero); - Node n = d_nodeManager->mkNode(PLUS, x, y, zTimesZero); + Node n = d_nodeManager->mkNode(ADD, x, y, zTimesZero); Node nExpected = n; Node nOut; diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index aee6a249b..329e4d569 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -153,7 +153,7 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval) /* Optimization objective: cost1 + cost2 */ - Node cost3 = d_nodeManager->mkNode(kind::PLUS, cost1, cost2); + Node cost3 = d_nodeManager->mkNode(kind::ADD, cost1, cost2); d_optslv->addObjective(cost3, OptimizationObjective::MINIMIZE); diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 284d686a9..e67954508 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -74,7 +74,7 @@ TEST_F(TestUtilWhiteArrayStoreAll, const_error) ASSERT_THROW( ArrayStoreAll(d_nodeManager->integerType(), d_nodeManager->mkNode( - kind::PLUS, + kind::ADD, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)), d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)))), IllegalArgumentException); -- 2.30.2