diff options
Diffstat (limited to 'src/preprocessing')
74 files changed, 460 insertions, 213 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 7d4351baa..382b1eb63 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -2,9 +2,9 @@ /*! \file assertion_pipeline.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Justin Xu, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index 77c5c4582..cc9d1c2af 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -2,9 +2,9 @@ /*! \file assertion_pipeline.h ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Justin Xu, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H -#define __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H +#ifndef CVC4__PREPROCESSING__ASSERTION_PIPELINE_H +#define CVC4__PREPROCESSING__ASSERTION_PIPELINE_H #include <vector> @@ -117,4 +117,4 @@ class AssertionPipeline } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */ +#endif /* CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */ diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index f5c3520d0..ddacc20c0 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -2,9 +2,9 @@ /*! \file apply_substs.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h index f2f77fd0e..f20ffa61e 100644 --- a/src/preprocessing/passes/apply_substs.h +++ b/src/preprocessing/passes/apply_substs.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H -#define __CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H +#ifndef CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H +#define CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/preprocessing/passes/apply_to_const.cpp b/src/preprocessing/passes/apply_to_const.cpp index 653a915d5..12591db0b 100644 --- a/src/preprocessing/passes/apply_to_const.cpp +++ b/src/preprocessing/passes/apply_to_const.cpp @@ -2,9 +2,9 @@ /*! \file apply_to_const.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/apply_to_const.h b/src/preprocessing/passes/apply_to_const.h index 9d5072023..4c1df22ca 100644 --- a/src/preprocessing/passes/apply_to_const.h +++ b/src/preprocessing/passes/apply_to_const.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H -#define __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H +#ifndef CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H +#define CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H #include <unordered_map> @@ -48,4 +48,4 @@ class ApplyToConst : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H */ +#endif /* CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H */ diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index 252ab941c..520e9f2a7 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -2,9 +2,9 @@ /*! \file bool_to_bv.cpp ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar, Makai Mann + ** Makai Mann, Yoni Zohar, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index da99d3c84..11cb551fa 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -2,9 +2,9 @@ /*! \file bool_to_bv.h ** \verbatim ** Top contributors (to current version): - ** Makai Mann, Yoni Zohar + ** Yoni Zohar, Makai Mann, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H -#define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H +#ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H +#define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -70,4 +70,4 @@ class BoolToBV : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */ +#endif /* CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */ diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp index 27648b45d..9c0d0ec68 100644 --- a/src/preprocessing/passes/bv_abstraction.cpp +++ b/src/preprocessing/passes/bv_abstraction.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h index 67e2ef296..b5840b355 100644 --- a/src/preprocessing/passes/bv_abstraction.h +++ b/src/preprocessing/passes/bv_abstraction.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -23,8 +23,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H -#define __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H +#define CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -47,4 +47,4 @@ class BvAbstraction : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */ +#endif /* CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */ diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp index 2ec49b985..c8cefcb17 100644 --- a/src/preprocessing/passes/bv_ackermann.cpp +++ b/src/preprocessing/passes/bv_ackermann.cpp @@ -2,9 +2,9 @@ /*! \file bv_ackermann.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Yoni Zohar, Aina Niemetz, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/bv_ackermann.h index 5f799ffe4..98d1080bd 100644 --- a/src/preprocessing/passes/bv_ackermann.h +++ b/src/preprocessing/passes/bv_ackermann.h @@ -2,9 +2,9 @@ /*! \file bv_ackermann.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -23,8 +23,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H -#define __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H +#define CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H #include <unordered_map> #include "expr/node.h" diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp index 8ee46829a..a16a8347d 100644 --- a/src/preprocessing/passes/bv_eager_atoms.cpp +++ b/src/preprocessing/passes/bv_eager_atoms.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h index 585c108fc..4ed685855 100644 --- a/src/preprocessing/passes/bv_eager_atoms.h +++ b/src/preprocessing/passes/bv_eager_atoms.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H -#define __CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H +#define CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -41,4 +41,4 @@ class BvEagerAtoms : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */ +#endif /* CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */ diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index 58e5f93bf..fccdfa2f9 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Aina Niemetz, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index 8ed5a884e..862777a9b 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H -#define __CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H +#define CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp index fb9ceac71..bfc02f332 100644 --- a/src/preprocessing/passes/bv_intro_pow2.cpp +++ b/src/preprocessing/passes/bv_intro_pow2.cpp @@ -2,9 +2,9 @@ /*! \file bv_intro_pow2.cpp ** \verbatim ** Top contributors (to current version): - ** Mathias Preiner + ** Mathias Preiner, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h index a5fe8e7bb..86d5ebfef 100644 --- a/src/preprocessing/passes/bv_intro_pow2.h +++ b/src/preprocessing/passes/bv_intro_pow2.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H -#define __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H +#define CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -42,4 +42,4 @@ class BvIntroPow2 : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */ +#endif /* CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */ diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index 811fe9251..3d3762ecd 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -2,9 +2,9 @@ /*! \file bv_to_bool.cpp ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar + ** Yoni Zohar, Liana Hadarean, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h index 2d138ee1d..dc0494943 100644 --- a/src/preprocessing/passes/bv_to_bool.h +++ b/src/preprocessing/passes/bv_to_bool.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Liana Hadarean, Yoni Zohar, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H -#define __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H +#define CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -76,4 +76,4 @@ class BVToBool : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */ +#endif /* CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */ diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp index 261a5f2ae..8bf4cc816 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.cpp +++ b/src/preprocessing/passes/extended_rewriter_pass.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h index f604a1af5..dbaaa05ad 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.h +++ b/src/preprocessing/passes/extended_rewriter_pass.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H -#define __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H +#ifndef CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H +#define CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -40,4 +40,4 @@ class ExtRewPre : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */ +#endif /* CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */ diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index 428360e8d..5e7d42632 100644 --- a/src/preprocessing/passes/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -2,9 +2,9 @@ /*! \file global_negate.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h index 0330aa10e..89c3a3e3e 100644 --- a/src/preprocessing/passes/global_negate.h +++ b/src/preprocessing/passes/global_negate.h @@ -2,9 +2,9 @@ /*! \file global_negate.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -22,8 +22,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H -#define __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H +#ifndef CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H +#define CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -49,4 +49,4 @@ class GlobalNegate : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */ +#endif /* CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */ diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index cc95bd1f2..150e41b8f 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h index 072e547c9..95f31621a 100644 --- a/src/preprocessing/passes/int_to_bv.h +++ b/src/preprocessing/passes/int_to_bv.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H -#define __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H +#ifndef CVC4__PREPROCESSING__PASSES__INT_TO_BV_H +#define CVC4__PREPROCESSING__PASSES__INT_TO_BV_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -42,4 +42,4 @@ class IntToBV : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H */ +#endif /* CVC4__PREPROCESSING__PASSES__INT_TO_BV_H */ diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index b70d2460d..bda38a6df 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -2,9 +2,9 @@ /*! \file ite_removal.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng + ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h index 27ec4f095..5620b4afb 100644 --- a/src/preprocessing/passes/ite_removal.h +++ b/src/preprocessing/passes/ite_removal.h @@ -2,9 +2,9 @@ /*! \file ite_removal.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng + ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H -#define __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H +#ifndef CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H +#define CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H #include <unordered_set> #include <vector> @@ -43,4 +43,4 @@ class IteRemoval : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif // __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H +#endif // CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 02f14f508..ad00ec204 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -2,9 +2,9 @@ /*! \file ite_simp.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Tim King, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index 2296d663e..44976bded 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H -#define __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H +#ifndef CVC4__PREPROCESSING__PASSES__ITE_SIMP_H +#define CVC4__PREPROCESSING__PASSES__ITE_SIMP_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 9a2dcca1f..37bc363f8 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -2,9 +2,9 @@ /*! \file miplib_trick.cpp ** \verbatim ** Top contributors (to current version): - ** Mathias Preiner + ** Mathias Preiner, Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index 7e75372a8..f1748d635 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H -#define __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H +#ifndef CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H +#define CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -59,4 +59,4 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H */ +#endif /* CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H */ diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index 744bd8ad8..a6da281ba 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h index 8d28b0742..7744df824 100644 --- a/src/preprocessing/passes/nl_ext_purify.h +++ b/src/preprocessing/passes/nl_ext_purify.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H -#define __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H +#ifndef CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H +#define CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H #include <unordered_map> #include <vector> @@ -54,4 +54,4 @@ class NlExtPurify : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */ +#endif /* CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */ diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index d8e1b3d66..4a0f38689 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -2,9 +2,9 @@ /*! \file non_clausal_simp.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index 2a244d7ad..cb4ece4a9 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H -#define __CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H +#ifndef CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H +#define CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H #include <vector> diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index 624b98ec1..d852f2d86 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.cpp +++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h index 5a91fef55..e73b721ff 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.h +++ b/src/preprocessing/passes/pseudo_boolean_processor.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H -#define __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H +#ifndef CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H +#define CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H #include <unordered_set> #include <vector> @@ -114,4 +114,4 @@ class PseudoBooleanProcessor : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif // __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H +#endif // CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 6bd94a3f0..0f71943c9 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -2,9 +2,9 @@ /*! \file quantifier_macros.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Kshitij Bansal + ** Andrew Reynolds, Yoni Zohar, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h index 092a62942..6b62c4d31 100644 --- a/src/preprocessing/passes/quantifier_macros.h +++ b/src/preprocessing/passes/quantifier_macros.h @@ -2,9 +2,9 @@ /*! \file quantifier_macros.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Yoni Zohar, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H -#define __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H +#ifndef CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H +#define CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H #include <map> #include <string> @@ -86,4 +86,4 @@ class QuantifierMacros : public PreprocessingPass } // preprocessing } // CVC4 -#endif /*__CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */ +#endif /*CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */ diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp index cfc4a8103..eb6017402 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.cpp +++ b/src/preprocessing/passes/quantifiers_preprocess.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Caleb Donovick ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h index 56ad2f175..991b3dd05 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.h +++ b/src/preprocessing/passes/quantifiers_preprocess.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Caleb Donovick ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -19,8 +19,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H -#define __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H +#ifndef CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H +#define CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -43,4 +43,4 @@ class QuantifiersPreprocess : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */ +#endif /* CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */ diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index 4b1fc06eb..ca47e3ea0 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h index eb4ac6593..7949fb051 100644 --- a/src/preprocessing/passes/real_to_int.h +++ b/src/preprocessing/passes/real_to_int.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H -#define __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H +#ifndef CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H +#define CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H #include <unordered_map> #include <vector> @@ -49,4 +49,4 @@ class RealToInt : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */ +#endif /* CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */ diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp index 4a5eccd4b..deb58ae9f 100644 --- a/src/preprocessing/passes/rewrite.cpp +++ b/src/preprocessing/passes/rewrite.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Caleb Donovick ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h index 1ab614fcd..e83cafb85 100644 --- a/src/preprocessing/passes/rewrite.h +++ b/src/preprocessing/passes/rewrite.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Caleb Donovick ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__REWRITE_H -#define __CVC4__PREPROCESSING__PASSES__REWRITE_H +#ifndef CVC4__PREPROCESSING__PASSES__REWRITE_H +#define CVC4__PREPROCESSING__PASSES__REWRITE_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -40,5 +40,5 @@ class Rewrite : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__REWRITE_H */ +#endif /* CVC4__PREPROCESSING__PASSES__REWRITE_H */ diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index 95a7995ce..a81dbb4b5 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -1,10 +1,10 @@ -/**********************/ +/********************* */ /*! \file sep_skolem_emp.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Yoni Zohar + ** Yoni Zohar, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h index 4a3dba6b8..1a5e36c40 100644 --- a/src/preprocessing/passes/sep_skolem_emp.h +++ b/src/preprocessing/passes/sep_skolem_emp.h @@ -2,9 +2,9 @@ /*! \file sep_skolem_emp.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Yoni Zohar + ** Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H -#define __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H +#ifndef CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H +#define CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -39,4 +39,4 @@ class SepSkolemEmp : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */ +#endif /* CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */ diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 807048696..d0612086c 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -2,9 +2,9 @@ /*! \file sort_infer.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h index 7c913e9cf..ae722529d 100644 --- a/src/preprocessing/passes/sort_infer.h +++ b/src/preprocessing/passes/sort_infer.h @@ -2,9 +2,9 @@ /*! \file sort_infer.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -12,8 +12,8 @@ ** \brief Sort inference preprocessing pass **/ -#ifndef __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ -#define __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ +#ifndef CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ +#define CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ #include <map> #include <string> @@ -46,4 +46,4 @@ class SortInferencePass : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */ +#endif /* CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */ diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index 26327fd5b..7af9f7fac 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h index ade1f5a33..f200755c5 100644 --- a/src/preprocessing/passes/static_learning.h +++ b/src/preprocessing/passes/static_learning.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H -#define __CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H +#ifndef CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H +#define CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -39,4 +39,4 @@ class StaticLearning : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H */ +#endif /* CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H */ diff --git a/src/preprocessing/passes/sygus_abduct.cpp b/src/preprocessing/passes/sygus_abduct.cpp new file mode 100644 index 000000000..346915b51 --- /dev/null +++ b/src/preprocessing/passes/sygus_abduct.cpp @@ -0,0 +1,174 @@ +/********************* */ +/*! \file sygus_abduct.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of sygus abduction preprocessing pass, which + ** transforms an arbitrary input into an abduction problem. + **/ + +#include "preprocessing/passes/sygus_abduct.h" + +#include "expr/node_algorithm.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +SygusAbduct::SygusAbduct(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "sygus-abduct"){}; + +PreprocessingPassResult SygusAbduct::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + NodeManager* nm = NodeManager::currentNM(); + Trace("sygus-abduct") << "Run sygus abduct..." << std::endl; + + Trace("sygus-abduct-debug") << "Collect symbols..." << std::endl; + std::unordered_set<Node, NodeHashFunction> symset; + std::vector<Node>& asserts = assertionsToPreprocess->ref(); + // do we have any assumptions, e.g. via check-sat-assuming? + bool usingAssumptions = (assertionsToPreprocess->getNumAssumptions() > 0); + // The following is our set of "axioms". We construct this set only when the + // usingAssumptions (above) is true. In this case, our input formula is + // partitioned into Fa ^ Fc as described in the header of this class, where: + // - The conjunction of assertions marked as assumptions are the negated + // conjecture Fc, and + // - The conjunction of all other assertions are the axioms Fa. + std::vector<Node> axioms; + for (size_t i = 0, size = asserts.size(); i < size; i++) + { + expr::getSymbols(asserts[i], symset); + // if we are not an assumption, add it to the set of axioms + if (usingAssumptions && i < assertionsToPreprocess->getAssumptionsStart()) + { + axioms.push_back(asserts[i]); + } + } + Trace("sygus-abduct-debug") + << "...finish, got " << symset.size() << " symbols." << std::endl; + + Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl; + std::vector<Node> syms; + std::vector<Node> vars; + std::vector<Node> varlist; + std::vector<TypeNode> varlistTypes; + for (const Node& s : symset) + { + TypeNode tn = s.getType(); + if (tn.isFirstClass()) + { + std::stringstream ss; + ss << s; + Node var = nm->mkBoundVar(tn); + syms.push_back(s); + vars.push_back(var); + Node vlv = nm->mkBoundVar(ss.str(), tn); + varlist.push_back(vlv); + varlistTypes.push_back(tn); + } + } + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Make abduction predicate..." << std::endl; + // make the abduction predicate to synthesize + TypeNode abdType = varlistTypes.empty() ? nm->booleanType() + : nm->mkPredicateType(varlistTypes); + Node abd = nm->mkBoundVar("A", abdType); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Make abduction predicate app..." << std::endl; + std::vector<Node> achildren; + achildren.push_back(abd); + achildren.insert(achildren.end(), vars.begin(), vars.end()); + Node abdApp = vars.empty() ? abd : nm->mkNode(APPLY_UF, achildren); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Set attributes..." << std::endl; + // set the sygus bound variable list + Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist); + abd.setAttribute(theory::SygusSynthFunVarListAttribute(), abvl); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Make conjecture body..." << std::endl; + Node input = asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts); + input = input.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); + // A(x) => ~input( x ) + input = nm->mkNode(OR, abdApp.negate(), input.negate()); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Make conjecture..." << std::endl; + Node res = input.negate(); + if (!vars.empty()) + { + Node bvl = nm->mkNode(BOUND_VAR_LIST, vars); + // exists x. ~( A( x ) => ~input( x ) ) + res = nm->mkNode(EXISTS, bvl, res); + } + // sygus attribute + Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); + theory::SygusAttribute ca; + sygusVar.setAttribute(ca, true); + Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); + std::vector<Node> iplc; + iplc.push_back(instAttr); + if (!axioms.empty()) + { + Node aconj = axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms); + aconj = + aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); + Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl; + Node sc = nm->mkNode(AND, aconj, abdApp); + Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars); + sc = nm->mkNode(EXISTS, vbvl, sc); + Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType()); + sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc); + instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar); + // build in the side condition + // exists x. A( x ) ^ input_axioms( x ) + // as an additional annotation on the sygus conjecture. In other words, + // the abducts A we procedure must be consistent with our axioms. + iplc.push_back(instAttr); + } + Node instAttrList = nm->mkNode(INST_PATTERN_LIST, iplc); + + Node fbvl = nm->mkNode(BOUND_VAR_LIST, abd); + + // forall A. exists x. ~( A( x ) => ~input( x ) ) + res = nm->mkNode(FORALL, fbvl, res, instAttrList); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + res = theory::Rewriter::rewrite(res); + + Trace("sygus-abduct") << "Generate: " << res << std::endl; + + Node trueNode = nm->mkConst(true); + + assertionsToPreprocess->replace(0, res); + for (size_t i = 1, size = assertionsToPreprocess->size(); i < size; ++i) + { + assertionsToPreprocess->replace(i, trueNode); + } + + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/sygus_abduct.h b/src/preprocessing/passes/sygus_abduct.h new file mode 100644 index 000000000..0e0868cda --- /dev/null +++ b/src/preprocessing/passes/sygus_abduct.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file sygus_abduct.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Sygus abduction preprocessing pass, which transforms an arbitrary + ** input into an abduction problem. + **/ + +#ifndef CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H +#define CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** SygusAbduct + * + * A preprocessing utility that turns a set of quantifier-free assertions into + * a sygus conjecture that encodes an abduction problem. In detail, if our + * input formula is F( x ) for free symbols x, then we construct the sygus + * conjecture: + * + * exists A. forall x. ( A( x ) => ~F( x ) ) + * + * where A( x ) is a predicate over the free symbols of our input. In other + * words, A( x ) is a sufficient condition for showing ~F( x ). + * + * Another way to view this is A( x ) is any condition such that A( x ) ^ F( x ) + * is unsatisfiable. + * + * A common use case is to find the weakest such A that meets the above + * specification. We do this by streaming solutions (sygus-stream) for A + * while filtering stronger solutions (sygus-filter-sol=strong). These options + * are enabled by default when this preprocessing class is used (sygus-abduct). + * + * If the input F( x ) is partitioned into axioms Fa and negated conjecture Fc + * Fa( x ) ^ Fc( x ), then the sygus conjecture we construct is: + * + * exists A. ( exists y. A( y ) ^ Fa( y ) ) ^ forall x. ( A( x ) => ~F( x ) ) + * + * In other words, A( y ) must be consistent with our axioms Fa and imply + * ~F( x ). We encode this conjecture using SygusSideConditionAttribute. + */ +class SygusAbduct : public PreprocessingPass +{ + public: + SygusAbduct(PreprocessingPassContext* preprocContext); + + protected: + /** + * Replaces the set of assertions by an abduction sygus problem described + * above. + */ + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */ diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index b0c374ff9..78e9e639a 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h index 5e7c6f7d0..91deb445c 100644 --- a/src/preprocessing/passes/sygus_inference.h +++ b/src/preprocessing/passes/sygus_inference.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -12,8 +12,8 @@ ** \brief SygusInference **/ -#ifndef __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ -#define __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ +#ifndef CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ +#define CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ #include <map> #include <string> @@ -68,4 +68,4 @@ class SygusInference : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ +#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ diff --git a/src/preprocessing/passes/symmetry_breaker.cpp b/src/preprocessing/passes/symmetry_breaker.cpp index 44fdd2c79..eb83fd229 100644 --- a/src/preprocessing/passes/symmetry_breaker.cpp +++ b/src/preprocessing/passes/symmetry_breaker.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Paul Meng, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/symmetry_breaker.h b/src/preprocessing/passes/symmetry_breaker.h index 9f0e7bb64..6bb10ebb8 100644 --- a/src/preprocessing/passes/symmetry_breaker.h +++ b/src/preprocessing/passes/symmetry_breaker.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Paul Meng, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -12,8 +12,8 @@ ** \brief Symmetry breaker for theories **/ -#ifndef __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ -#define __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ +#ifndef CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ +#define CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ #include <map> #include <string> @@ -106,4 +106,4 @@ class SymBreakerPass : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ */ +#endif /* CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ */ diff --git a/src/preprocessing/passes/symmetry_detect.cpp b/src/preprocessing/passes/symmetry_detect.cpp index ec784a6ba..8d0d04149 100644 --- a/src/preprocessing/passes/symmetry_detect.cpp +++ b/src/preprocessing/passes/symmetry_detect.cpp @@ -2,9 +2,9 @@ /*! \file symmetry_detect.cpp ** \verbatim ** Top contributors (to current version): - ** Paul Meng + ** Andrew Reynolds, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h index 67e40da00..07a545723 100644 --- a/src/preprocessing/passes/symmetry_detect.h +++ b/src/preprocessing/passes/symmetry_detect.h @@ -2,9 +2,9 @@ /*! \file symmetry_detect.h ** \verbatim ** Top contributors (to current version): - ** Paul Meng + ** Andrew Reynolds, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H -#define __CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H +#ifndef CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H +#define CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H #include <map> #include <string> diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 7e687329b..3eb27c2f7 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -2,9 +2,9 @@ /*! \file synth_rew_rules.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -79,8 +79,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( { Trace("srs-input-debug") << "...preprocess " << cur << std::endl; visited[cur] = false; - Kind k = cur.getKind(); - bool isQuant = k == FORALL || k == EXISTS || k == LAMBDA || k == CHOICE; + bool isQuant = cur.isClosure(); // we recurse on this node if it is not a quantified formula if (!isQuant) { diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h index 2b05bbf00..38ef98b35 100644 --- a/src/preprocessing/passes/synth_rew_rules.h +++ b/src/preprocessing/passes/synth_rew_rules.h @@ -2,9 +2,9 @@ /*! \file synth_rew_rules.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -13,8 +13,8 @@ ** where t1 and t2 are subterms of the input. **/ -#ifndef __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H -#define __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H +#ifndef CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H +#define CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -74,4 +74,4 @@ class SynthRewRulesPass : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */ +#endif /* CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */ diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 3a5213f43..1399363fa 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -1,10 +1,10 @@ /********************* */ -/*! \file bv_abstraction.cpp +/*! \file theory_preprocess.cpp ** \verbatim ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h index 58eaee611..cfa9ab0b5 100644 --- a/src/preprocessing/passes/theory_preprocess.h +++ b/src/preprocessing/passes/theory_preprocess.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H -#define __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H +#ifndef CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H +#define CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -40,4 +40,4 @@ class TheoryPreprocess : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */ +#endif /* CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */ diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index f58f1a44b..c41f1fca9 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -2,9 +2,9 @@ /*! \file unconstrained_simplifier.cpp ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Tim King, Andrew Reynolds + ** Clark Barrett, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index 658834ee3..ac4fd0a03 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -2,9 +2,9 @@ /*! \file unconstrained_simplifier.h ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Tim King + ** Clark Barrett, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H -#define __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H +#ifndef CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H +#define CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H #include <unordered_map> #include <unordered_set> diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 120c68a91..84c3ca79b 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -2,9 +2,9 @@ /*! \file preprocessing_pass.cpp ** \verbatim ** Top contributors (to current version): - ** Justin Xu, Aina Niemetz + ** Justin Xu, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index 448cacb87..4a2e71488 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -2,9 +2,9 @@ /*! \file preprocessing_pass.h ** \verbatim ** Top contributors (to current version): - ** Justin Xu, Aina Niemetz + ** Justin Xu ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -28,8 +28,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_H -#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_H +#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_H +#define CVC4__PREPROCESSING__PREPROCESSING_PASS_H #include <string> @@ -82,4 +82,4 @@ class PreprocessingPass { } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_H */ +#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_H */ diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 3f72a4559..2d25502d1 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -2,9 +2,9 @@ /*! \file preprocessing_pass_context.cpp ** \verbatim ** Top contributors (to current version): - ** Justin Xu, Mathias Preiner, Aina Niemetz + ** Aina Niemetz, Mathias Preiner, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 3eb0f10b5..e37680538 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -2,9 +2,9 @@ /*! \file preprocessing_pass_context.h ** \verbatim ** Top contributors (to current version): - ** Justin Xu, Andres Noetzli, Aina Niemetz + ** Aina Niemetz, Mathias Preiner, Justin Xu ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H -#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H +#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H +#define CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H #include "context/cdo.h" #include "context/context.h" @@ -121,4 +121,4 @@ class PreprocessingPassContext } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */ +#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index f2e7c8603..15618f575 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -2,9 +2,9 @@ /*! \file preprocessing_pass_registry.cpp ** \verbatim ** Top contributors (to current version): - ** Justin Xu, Yoni Zohar + ** Andres Noetzli, Justin Xu, Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -48,6 +48,7 @@ #include "preprocessing/passes/sep_skolem_emp.h" #include "preprocessing/passes/sort_infer.h" #include "preprocessing/passes/static_learning.h" +#include "preprocessing/passes/sygus_abduct.h" #include "preprocessing/passes/sygus_inference.h" #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" @@ -126,6 +127,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>); registerPassInfo("real-to-int", callCtor<RealToInt>); registerPassInfo("sygus-infer", callCtor<SygusInference>); + registerPassInfo("sygus-abduct", callCtor<SygusAbduct>); registerPassInfo("bv-to-bool", callCtor<BVToBool>); registerPassInfo("bv-intro-pow2", callCtor<BvIntroPow2>); registerPassInfo("sort-inference", callCtor<SortInferencePass>); diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h index e6c98c1f9..9cc109897 100644 --- a/src/preprocessing/preprocessing_pass_registry.h +++ b/src/preprocessing/preprocessing_pass_registry.h @@ -2,9 +2,9 @@ /*! \file preprocessing_pass_registry.h ** \verbatim ** Top contributors (to current version): - ** Justin Xu, Yoni Zohar + ** Andres Noetzli, Justin Xu, Yoni Zohar ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,8 +16,8 @@ **/ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H -#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H +#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H +#define CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H #include <memory> #include <string> @@ -97,4 +97,4 @@ class PreprocessingPassRegistry { } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */ +#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */ diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 66d9151df..9c3db0b0d 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -2,9 +2,9 @@ /*! \file ite_utilities.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Aina Niemetz, Andres Noetzli + ** Tim King, Aina Niemetz, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h index e137749db..ad195e62e 100644 --- a/src/preprocessing/util/ite_utilities.h +++ b/src/preprocessing/util/ite_utilities.h @@ -2,9 +2,9 @@ /*! \file ite_utilities.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Aina Niemetz, Paul Meng + ** Tim King, Aina Niemetz, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -20,8 +20,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__ITE_UTILITIES_H -#define __CVC4__ITE_UTILITIES_H +#ifndef CVC4__ITE_UTILITIES_H +#define CVC4__ITE_UTILITIES_H #include <unordered_map> #include <vector> |