diff options
Diffstat (limited to 'src/prop')
33 files changed, 511 insertions, 496 deletions
diff --git a/src/prop/bv_sat_solver_notify.h b/src/prop/bv_sat_solver_notify.h index df698c722..45fbf1699 100644 --- a/src/prop/bv_sat_solver_notify.h +++ b/src/prop/bv_sat_solver_notify.h @@ -1,17 +1,18 @@ -/********************* */ -/*! \file bv_sat_solver_notify.h - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Alex Ozdemir, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 The interface for things that want to recieve notification from the - ** SAT solver - **/ +/****************************************************************************** + * Top contributors (to current version): + * Liana Hadarean, Alex Ozdemir, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * The interface for things that want to recieve notification from the SAT + * solver. + */ #include "cvc4_private.h" diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index ba1a7fc3b..57b248ddf 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file bvminisat.cpp - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Dejan Jovanovic, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 SAT Solver. - ** - ** Implementation of the minisat for cvc4 (bitvectors). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Liana Hadarean, Dejan Jovanovic, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * SAT Solver. + * + * Implementation of the minisat for cvc4 (bit-vectors). + */ #include "prop/bvminisat/bvminisat.h" diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 1bc0eb237..e7dc3ef0c 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file bvminisat.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Liana Hadarean, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 SAT Solver. - ** - ** Implementation of the minisat for cvc4 (bitvectors). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Liana Hadarean, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * SAT Solver. + * + * Implementation of the minisat for cvc4 (bit-vectors). + */ #include "cvc4_private.h" diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index 5abdada71..9cbf067a6 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file cadical.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Andres Noetzli, Liana Hadarean - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 Wrapper for CaDiCaL SAT Solver. - ** - ** Implementation of the CaDiCaL SAT solver for CVC4 (bitvectors). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Andres Noetzli, Liana Hadarean + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Wrapper for CaDiCaL SAT Solver. + * + * Implementation of the CaDiCaL SAT solver for CVC4 (bit-vectors). + */ #include "prop/cadical.h" diff --git a/src/prop/cadical.h b/src/prop/cadical.h index e8a36d0a0..f046d66e4 100644 --- a/src/prop/cadical.h +++ b/src/prop/cadical.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file cadical.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Aina Niemetz, Liana Hadarean - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 Wrapper for CaDiCaL SAT Solver. - ** - ** Implementation of the CaDiCaL SAT solver for CVC4 (bitvectors). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Aina Niemetz, Liana Hadarean + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Wrapper for CaDiCaL SAT Solver. + * + * Implementation of the CaDiCaL SAT solver for CVC4 (bit-vectors). + */ #include "cvc4_private.h" diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 111c6c2df..8603d5ca3 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -1,20 +1,18 @@ -/********************* */ -/*! \file cnf_stream.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Haniel Barbosa, Liana Hadarean - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 A CNF converter that takes in asserts and has the side effect - ** of given an equisatisfiable stream of assertions to PropEngine. - ** - ** A CNF converter that takes in asserts and has the side effect - ** of given an equisatisfiable stream of assertions to PropEngine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Haniel Barbosa, Liana Hadarean + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * A CNF converter that takes in asserts and has the side effect of given an + * equisatisfiable stream of assertions to PropEngine. + */ #include "prop/cnf_stream.h" #include <queue> diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 4b41ad691..64a735fec 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -1,24 +1,25 @@ -/********************* */ -/*! \file cnf_stream.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Haniel Barbosa, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 This class transforms a sequence of formulas into clauses. - ** - ** This class takes a sequence of formulas. - ** It outputs a stream of clauses that is propositionally - ** equi-satisfiable with the conjunction of the formulas. - ** This stream is maintained in an online fashion. - ** - ** Unlike other parts of the system it is aware of the PropEngine's - ** internals such as the representation and translation of [??? -Chris] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Haniel Barbosa, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * This class transforms a sequence of formulas into clauses. + * + * This class takes a sequence of formulas. + * It outputs a stream of clauses that is propositionally + * equi-satisfiable with the conjunction of the formulas. + * This stream is maintained in an online fashion. + * + * Unlike other parts of the system it is aware of the PropEngine's + * internals such as the representation and translation of [??? -Chris] + */ #include "cvc4_private.h" diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index 5e0b056dc..ed2993622 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file cryptominisat.cpp - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Mathias Preiner, Alex Ozdemir - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 SAT Solver. - ** - ** Implementation of the cryptominisat for cvc4 (bitvectors). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Liana Hadarean, Mathias Preiner, Alex Ozdemir + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * SAT Solver. + * + * Implementation of the cryptominisat for cvc4 (bit-vectors). + */ #ifdef CVC5_USE_CRYPTOMINISAT diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index b217cee9c..40a681148 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file cryptominisat.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Liana Hadarean, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 SAT Solver. - ** - ** Implementation of the cryptominisat sat solver for cvc4 (bitvectors). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Liana Hadarean, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * SAT Solver. + * + * Implementation of the cryptominisat sat solver for cvc4 (bit-vectors). + */ #include "cvc4_private.h" diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp index 949af2901..8c9b80888 100644 --- a/src/prop/kissat.cpp +++ b/src/prop/kissat.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file kissat.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 Wrapper for Kissat SAT Solver. - ** - ** Wrapper for the Kissat SAT solver (for theory of bit-vectors). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Wrapper for Kissat SAT Solver. + * + * Wrapper for the Kissat SAT solver (for theory of bit-vectors). + */ #include "prop/kissat.h" diff --git a/src/prop/kissat.h b/src/prop/kissat.h index b2bc8e074..3b65a06bb 100644 --- a/src/prop/kissat.h +++ b/src/prop/kissat.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file kissat.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 Wrapper for Kissat SAT Solver. - ** - ** Wrapper for the Kissat SAT solver (for theory of bit-vectors). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Wrapper for Kissat SAT Solver. + * + * Wrapper for the Kissat SAT solver (for theory of bit-vectors). + */ #include "cvc4_private.h" diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 07b345eda..e84325897 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file minisat.cpp - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Dejan Jovanovic, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 SAT Solver. - ** - ** Implementation of the minisat interface for cvc4. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Liana Hadarean, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * SAT Solver. + * + * Implementation of the minisat interface for cvc5. + */ #include "prop/minisat/minisat.h" diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 0a36b6297..36f468f90 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file minisat.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Haniel Barbosa, Liana Hadarean - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 SAT Solver. - ** - ** Implementation of the minisat interface for cvc4. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Haniel Barbosa, Liana Hadarean + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * SAT Solver. + * + * Implementation of the minisat interface for cvc5. + */ #pragma once diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index 8527950ce..b7d80da76 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_cnf_stream.cpp - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, Andrew Reynolds, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 the proof-producing CNF stream - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Andrew Reynolds, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementation of the proof-producing CNF stream. + */ #include "prop/proof_cnf_stream.h" diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index 5848c64f0..d696db580 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_cnf_stream.h - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, Dejan Jovanovic, Liana Hadarean - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 The proof-producing CNF stream - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Dejan Jovanovic, Liana Hadarean + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * The proof-producing CNF stream. + */ #include "cvc4_private.h" diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp index 10bf53aa1..596d2f7d9 100644 --- a/src/prop/proof_post_processor.cpp +++ b/src/prop/proof_post_processor.cpp @@ -1,17 +1,17 @@ -/********************* */ -/*! \file proof_post_processor.cpp - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 the module for processing proof nodes in the prop - ** engine - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementation of the module for processing proof nodes in the prop engine. + */ #include "prop/proof_post_processor.h" diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h index 68b6d3a42..1ec980868 100644 --- a/src/prop/proof_post_processor.h +++ b/src/prop/proof_post_processor.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_post_processor.h - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 The module for processing proof nodes in the prop engine - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * The module for processing proof nodes in the prop engine. + */ #include "cvc4_private.h" diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 65d20d9a0..866110e5d 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file prop_engine.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 the propositional engine of CVC4 - ** - ** Implementation of the propositional engine of CVC4. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementation of the propositional engine of cvc5. + */ #include "prop/prop_engine.h" diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 773b27de4..2beb633ee 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -1,20 +1,19 @@ -/********************* */ -/*! \file prop_engine.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 The PropEngine (propositional engine); main interface point - ** between CVC4's SMT infrastructure and the SAT solver - ** - ** The PropEngine (propositional engine); main interface point - ** between CVC4's SMT infrastructure and the SAT solver. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Dejan Jovanovic + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * The PropEngine (propositional engine). + * + * Main interface point between cvc5's SMT infrastructure and the SAT solver. + */ #include "cvc4_private.h" diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp index 08c13fe5f..000cebb72 100644 --- a/src/prop/prop_proof_manager.cpp +++ b/src/prop/prop_proof_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file prop_proof_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 the proof manager for the PropPfManager - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementation of the proof manager for the PropPfManager. + */ #include "prop/prop_proof_manager.h" diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h index 45136085d..e6435213c 100644 --- a/src/prop/prop_proof_manager.h +++ b/src/prop/prop_proof_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file prop_proof_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 The proof manager of PropEngine - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * The proof manager of PropEngine. + */ #include "cvc4_private.h" diff --git a/src/prop/registrar.h b/src/prop/registrar.h index daa364bcb..7b3419a0d 100644 --- a/src/prop/registrar.h +++ b/src/prop/registrar.h @@ -1,22 +1,22 @@ -/********************* */ -/*! \file registrar.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Liana Hadarean, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 Class to encapsulate preregistration duties - ** - ** Class to encapsulate preregistration duties. This class permits the - ** CNF stream implementation to reach into the theory engine to - ** preregister only those terms with an associated SAT literal (at the - ** point when they get the SAT literal), without having to refer to the - ** TheoryEngine class directly. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Liana Hadarean, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Class to encapsulate preregistration duties + * + * This class permits the CNF stream implementation to reach into the theory + * engine to preregister only those terms with an associated SAT literal (at + * the point when they get the SAT literal), without having to refer to the + * TheoryEngine class directly. + */ #include "cvc4_private.h" diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index ec29d6bd5..00abb0b8f 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sat_proof_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 the proof manager for Minisat - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementation of the proof manager for Minisat. + */ #include "prop/sat_proof_manager.h" diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 426771a37..9cd5f944b 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sat_proof_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 The proof manager for Minisat - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * The proof manager for Minisat. + */ #include "cvc4_private.h" diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index ae87d1396..ec2ebcd3e 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file sat_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Liana Hadarean, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 SAT Solver. - ** - ** SAT Solver. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Liana Hadarean, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * SAT Solver. + */ #include "cvc4_private.h" diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 90eec9153..3ae6dae1c 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file sat_solver_factory.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Aina Niemetz, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 SAT Solver creation facility. - ** - ** SAT Solver. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Aina Niemetz, Dejan Jovanovic + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * SAT Solver creation facility. + */ #include "prop/sat_solver_factory.h" diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index cebbe6e27..413b0280c 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file sat_solver_factory.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Liana Hadarean, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 SAT Solver. - ** - ** SAT Solver creation facility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Liana Hadarean, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * SAT Solver creation facility + */ #include "cvc4_private.h" diff --git a/src/prop/sat_solver_types.cpp b/src/prop/sat_solver_types.cpp index 13494221e..a597ed53f 100644 --- a/src/prop/sat_solver_types.cpp +++ b/src/prop/sat_solver_types.cpp @@ -1,18 +1,18 @@ -/********************* */ -/*! \file sat_solver_types.cpp - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 Implementations of SAT solver type operations which require large - ** std headers. - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Alex Ozdemir + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementations of SAT solver type operations which require large std + * headers. + */ #include "prop/sat_solver_types.h" diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index 0ab0cba53..20dc9a775 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -1,24 +1,25 @@ -/********************* */ -/*! \file sat_solver_types.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Alex Ozdemir, Liana Hadarean - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 This class transforms a sequence of formulas into clauses. - ** - ** This class takes a sequence of formulas. - ** It outputs a stream of clauses that is propositionally - ** equi-satisfiable with the conjunction of the formulas. - ** This stream is maintained in an online fashion. - ** - ** Unlike other parts of the system it is aware of the PropEngine's - ** internals such as the representation and translation of [??? -Chris] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Alex Ozdemir, Liana Hadarean + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * This class transforms a sequence of formulas into clauses. + * + * This class takes a sequence of formulas. + * It outputs a stream of clauses that is propositionally + * equi-satisfiable with the conjunction of the formulas. + * This stream is maintained in an online fashion. + * + * Unlike other parts of the system it is aware of the PropEngine's + * internals such as the representation and translation of [??? -Chris] + */ #pragma once diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp index dbc640d8c..9b4011557 100644 --- a/src/prop/skolem_def_manager.cpp +++ b/src/prop/skolem_def_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file skolem_def_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 Skolem definition manager - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Skolem definition manager. + */ #include "prop/skolem_def_manager.h" diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h index 1b7b9b4dc..6165ee593 100644 --- a/src/prop/skolem_def_manager.h +++ b/src/prop/skolem_def_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file skolem_def_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 Skolem definition manager - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Skolem definition manager. + */ #include "cvc4_private.h" diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index e509bf182..dffd36fd5 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file theory_proxy.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Dejan Jovanovic + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "prop/theory_proxy.h" #include "context/context.h" diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 9affec6d0..e468930e7 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_proxy.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Dejan Jovanovic, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 SAT Solver. - ** - ** SAT Solver. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Dejan Jovanovic, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * SAT Solver. + */ #include "cvc4_private.h" |