diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/theory/arith | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/theory/arith')
24 files changed, 179 insertions, 29 deletions
diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp index 872c25e3b..3b1f5f395 100644 --- a/src/theory/arith/arith_priority_queue.cpp +++ b/src/theory/arith/arith_priority_queue.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_priority_queue.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/arith_priority_queue.h" diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index f912d7753..1e7e3460b 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_priority_queue.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_private.h" diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp index 7f38c74a7..d1fce5b90 100644 --- a/src/theory/arith/arith_prop_manager.cpp +++ b/src/theory/arith/arith_prop_manager.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_prop_manager.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/arith_prop_manager.h" diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h index 39bcb7477..82f58c7a0 100644 --- a/src/theory/arith/arith_prop_manager.h +++ b/src/theory/arith/arith_prop_manager.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_prop_manager.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_private.h" #ifndef __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 8d12e78fe..66223b479 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -2,8 +2,8 @@ /*! \file arith_rewriter.cpp ** \verbatim ** Original author: taking - ** Major contributors: dejan - ** Minor contributors (to current version): mdeters + ** Major contributors: none + ** Minor contributors (to current version): mdeters, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index c58778215..03402a6f1 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -2,8 +2,8 @@ /*! \file arith_static_learner.h ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 2dee26be4..3a1135f74 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/atom_database.cpp b/src/theory/arith/atom_database.cpp index 5c3519435..774d0eb22 100644 --- a/src/theory/arith/atom_database.cpp +++ b/src/theory/arith/atom_database.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/atom_database.h b/src/theory/arith/atom_database.h index 25020977a..af7068ada 100644 --- a/src/theory/arith/atom_database.h +++ b/src/theory/arith/atom_database.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index d0e4ed1f4..c5c5c629b 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index c70d26db5..c8a5e39a7 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index db47062bb..bf5ea24c1 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -5,6 +5,7 @@ # theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h" +typechecker "theory/arith/theory_arith_type_rules.h" properties stable-infinite properties check propagate staticLearning presolve notifyRestart @@ -17,6 +18,7 @@ operator MULT 2: "arithmetic multiplication" operator MINUS 2 "arithmetic binary subtraction operator" operator UMINUS 1 "arithmetic unary negation" operator DIVISION 2 "arithmetic division" +operator POW 2 "arithmetic power" sort REAL_TYPE \ Cardinality::REALS \ @@ -58,4 +60,19 @@ operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" operator GEQ 2 "greater than or equal, x >= y" +typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule +typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule +typerule MINUS ::CVC4::theory::arith::ArithOperatorTypeRule +typerule UMINUS ::CVC4::theory::arith::ArithOperatorTypeRule +typerule DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule +typerule POW ::CVC4::theory::arith::ArithOperatorTypeRule + +typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule +typerule CONST_INTEGER ::CVC4::theory::arith::ArithConstantTypeRule + +typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule +typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule +typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule +typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule + endtheory diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index b529a8077..e7df14df7 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index d6e79318d..6e2d706cc 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h index e44ba8687..c126ab568 100644 --- a/src/theory/arith/ordered_set.h +++ b/src/theory/arith/ordered_set.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file ordered_set.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include <map> #include <set> #include "expr/kind.h" diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 3cd8ed926..ed8f837d1 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index f07e524aa..aa333046b 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 3e2d90674..77e7e1060 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file simplex.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/simplex.h" diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index b3f43baf1..04b4ca784 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file simplex.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_private.h" diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index b432416bd..ef3206650 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index e14436f8c..3da3d68a5 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -2,10 +2,10 @@ /*! \file tableau.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan + ** Major contributors: none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 2664aaac3..4369c6de0 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2,10 +2,10 @@ /*! \file theory_arith.cpp ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): barrett, dejan, mdeters + ** Major contributors: mdeters, dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 7e14f6b06..2e85659e4 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: mdeters ** Major contributors: taking - ** Minor contributors (to current version): barrett + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 8bfd2aef6..9c69ec684 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters, cconway ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing |