Generate multiple patterns with circuit_validator (lsils#368)

* generate_pattern

* add test cases & API with signal

* update docs

docs/algorithms/circuit_validator.rst

@@ -79,3 +79,13 @@ The following code shows how to check functional equivalence of a root node to s
 **Updating**
 
 .. doxygenfunction:: mockturtle::circuit_validator::update
+
+**Generate multiple patterns**
+
+A simulation pattern is a collection of value assignments to every primary inputs.
+A counter-example of a failing validation is a simulation pattern under which the nodes being validated have different simulation values. 
+It can be directly read from the public data member ``circuit_validator::cex`` (which is a ``std::vector<bool>`` of size ``Ntk::num_pis()``) after a call to (any type of) ``circuit_validator::validate`` which returns ``false``.
+If multiple different patterns are desired, one can call ``circuit_validator::generate_pattern``. However, this is currently only supported for constant validation.
+
+.. doxygenfunction:: mockturtle::circuit_validator::generate_pattern( signal const&, bool, std::vector<std::vector<bool>> const&, uint32_t )
+.. doxygenfunction:: mockturtle::circuit_validator::generate_pattern( node const&, bool, std::vector<std::vector<bool>> const&, uint32_t )

docs/algorithms/simulation.rst

@@ -78,8 +78,8 @@ The following simulators are implemented:
 Partial simulation
 ~~~~~~~~~~~~~~~~~~
 
-With `partial_simulator`, adding new simulation patterns and re-simulation can be done.
-Incremental simulation is adopted, which speeds up simulation time by only re-simulating needed nodes and only re-computing the last block of `partial_truth_table`.
+With ``partial_simulator``, adding new simulation patterns and re-simulation can be done.
+Incremental simulation is adopted, which speeds up simulation time by only re-simulating needed nodes and only re-computing the last block of ``partial_truth_table``.
 Note that currently only AIG and XAG are supported.
 
 .. doxygenfunction:: mockturtle::partial_simulator::partial_simulator( unsigned, unsigned, std::default_random_engine::result_type )

include/mockturtle/algorithms/circuit_validator.hpp

@@ -251,7 +251,6 @@ class circuit_validator
  {
  construct( root );
  }
- assert( literals[root].variable() != bill::var_type( 0 ) );
 
  std::optional<bool> res;
  if constexpr ( use_odc )
@@ -285,6 +284,71 @@ class circuit_validator
  return res;
  }
 
+ /*! \brief Generate pattern(s) for signal `f` to be `value`, optionally blocking several known patterns. 
+ *
+ * Requires `use_pushpop = true`.
+ *
+ * If `block_patterns` and the returned vector are both empty, `f` is validated to be a constant of `!value`.
+ *
+ * \param block_patterns Patterns to be blocked in the solver. (Will not generate any of them.)
+ * \param num_patterns Number of patterns to be generated, if possible. (The size of the result may be smaller than this number, but never larger.)
+ */
+ template<bool enabled = use_pushpop, typename = std::enable_if_t<enabled>>
+ std::vector<std::vector<bool>> generate_pattern( signal const& f, bool value, std::vector<std::vector<bool>> const& block_patterns = {}, uint32_t num_patterns = 1u )
+ {
+ return generate_pattern( ntk.get_node( f ), value ^ ntk.is_complemented( f ), block_patterns, num_patterns );
+ }
+
+ /*! \brief Generate pattern(s) for node `root` to be `value`, optionally blocking several known patterns. */
+ template<bool enabled = use_pushpop, typename = std::enable_if_t<enabled>>
+ std::vector<std::vector<bool>> generate_pattern( node const& root, bool value, std::vector<std::vector<bool>> const& block_patterns = {}, uint32_t num_patterns = 1u )
+ {
+ if ( !literals.has( root ) )
+ {
+ construct( root );
+ }
+
+ solver.push();
+
+ for ( auto const& pattern : block_patterns )
+ {
+ block_pattern( pattern );
+ }
+
+ std::vector<bill::lit_type> assumptions( {lit_not_cond( literals[root], !value )} );
+ if constexpr ( use_odc )
+ {
+ if ( ps.odc_levels != 0 )
+ {
+ assumptions.emplace_back( build_odc_window( root, ~literals[root] ) );
+ }
+ }
+
+ std::optional<bool> res;
+ std::vector<std::vector<bool>> generated;
+ for ( auto i = 0u; i < num_patterns; ++i )
+ {
+ res = solve( assumptions );
+
+ if ( !res || *res ) /* timeout or UNSAT */
+ {
+ break;
+ }
+ else /* SAT */
+ {
+ generated.emplace_back( cex );
+ block_pattern( cex );
+ }
+ }
+
+ solver.pop();
+ if ( solver.num_clauses() > ps.max_clauses )
+ {
+ restart();
+ }
+ return generated;
+ }
+
  /*! \brief Update CNF clauses.
  *
  * This function should be called when the function of one or more nodes
@@ -317,20 +381,8 @@ class circuit_validator
  literals[n] = bill::lit_type( i + 1, bill::lit_type::polarities::positive );
  } );
 
- /* compute literals for nodes */
- //uint32_t next_var = ntk.num_pis() + 1;
- //ntk.foreach_gate( [&]( auto const& n ) {
- // literals[n] = bill::lit_type( next_var++, bill::lit_type::polarities::positive );
- //} );
-
  solver.add_variables( ntk.num_pis() + 1 );
  solver.add_clause( {~literals[ntk.get_constant( false )]} );
-
- //generate_cnf<Ntk, bill::lit_type>(
- // ntk, [&]( auto const& clause ) {
- // solver.add_clause( clause );
- // },
- // literals );
  }
 
  void construct( node const& n )
@@ -461,7 +513,6 @@ class circuit_validator
  {
  construct( root );
  }
- assert( literals[root].variable() != bill::var_type( 0 ) );
 
  std::optional<bool> res;
  if constexpr ( use_odc )
@@ -497,6 +548,16 @@ class circuit_validator
  return res;
  }
 
+ void block_pattern( std::vector<bool> const& pattern )
+ {
+ assert( pattern.size() == ntk.num_pis() );
+ std::vector<bill::lit_type> clause;
+ ntk.foreach_pi( [&]( auto const& n, auto i ) {
+ clause.emplace_back( lit_not_cond( literals[n] , pattern[i] ) );
+ } );
+ solver.add_clause( clause );
+ }
+
 private:
  template<bool enabled = use_odc, typename = std::enable_if_t<enabled>>
  bill::lit_type build_odc_window( node const& root, bill::lit_type const& lit )

test/algorithms/circuit_validator.cpp

@@ -116,12 +116,43 @@ TEST_CASE( "Validating const nodes", "[validator]" )
 
  circuit_validator v( aig );
 
+ /* several APIs are available */
  CHECK( *( v.validate( aig.get_node( h ), false ) ) == true );
+ CHECK( *( v.validate( h, false ) ) == true );
+ CHECK( *( v.validate( aig.get_constant( false ), h ) ) == true );
+
  CHECK( *( v.validate( f1, false ) ) == false );
  CHECK( v.cex[0] == false );
  CHECK( v.cex[1] == true );
 }
 
+TEST_CASE( "Generate multiple patterns", "[validator]" )
+{
+ /* original circuit */
+ aig_network aig;
+ auto const a = aig.create_pi();
+ auto const b = aig.create_pi();
+ auto const c = aig.create_pi();
+ auto const f1 = aig.create_xor( a, b );
+ auto const f2 = aig.create_xor( f1, c ); // a ^ b ^ c
+
+ circuit_validator<aig_network, bill::solvers::bsat2, true, false, false> v( aig );
+
+ CHECK( *( v.validate( f2, false ) ) == false ); /* f2 is not a constant 0 */
+ std::vector<std::vector<bool>> block_pattern( {v.cex} );
+ auto const patterns = v.generate_pattern( f2, true, block_pattern, 10 ); /* generate patterns making f2 = 1 */
+ CHECK( patterns.size() == 3u );
+ for ( auto const& pattern : patterns )
+ {
+ CHECK( ( pattern[0] ^ pattern[1] ^ pattern[2] ) == true );
+ CHECK( pattern != block_pattern[0] );
+ }
+
+ /* blocking patterns should not affect later validations */
+ CHECK( *( v.validate( f1, false ) ) == false ); /* f1 is not a constant 0 */
+ CHECK( ( v.cex[0] ^ v.cex[1] ) == true );
+}
+
 TEST_CASE( "Validating with ODC", "[validator]" )
 {
  /* original circuit */